diff --git a/core/src/eval/merge.rs b/core/src/eval/merge.rs
index 9257988eb8..503f3a6a74 100644
--- a/core/src/eval/merge.rs
+++ b/core/src/eval/merge.rs
@@ -415,7 +415,7 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a LocIdent> + Clon
     let mut pending_contracts = pending_contracts1.revert_closurize(cache, env_final, env1.clone());
 
     for ctr2 in pending_contracts2.revert_closurize(cache, env_final, env2.clone()) {
-        RuntimeContract::push_elide(
+        RuntimeContract::push_dedup(
             initial_env,
             &mut pending_contracts,
             &env_final,
@@ -427,7 +427,7 @@ fn merge_fields<'a, C: Cache, I: DoubleEndedIterator<Item = &'a LocIdent> + Clon
     Ok(Field {
         metadata: FieldMetadata {
             doc: merge_doc(metadata1.doc, metadata2.doc),
-            annotation: TypeAnnotation::combine_elide(metadata1.annotation, metadata2.annotation),
+            annotation: TypeAnnotation::combine_dedup(metadata1.annotation, metadata2.annotation),
             // If one of the record requires this field, then it musn't be optional. The
             // resulting field is optional iff both are.
             opt: metadata1.opt && metadata2.opt,
diff --git a/core/src/eval/operation.rs b/core/src/eval/operation.rs
index c4fab4ef4a..47736e2647 100644
--- a/core/src/eval/operation.rs
+++ b/core/src/eval/operation.rs
@@ -2132,7 +2132,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                                         label: label.clone(),
                                     };
 
-                                crate::term::RuntimeContract::push_elide(
+                                crate::term::RuntimeContract::push_dedup(
                                     &self.initial_env,
                                     &mut field.pending_contracts,
                                     &term_original_env,
diff --git a/core/src/term/mod.rs b/core/src/term/mod.rs
index ff49b1fc60..9e072652c2 100644
--- a/core/src/term/mod.rs
+++ b/core/src/term/mod.rs
@@ -325,27 +325,24 @@ impl RuntimeContract {
     /// Push a pending contract to a vector of contracts if the contract to add isn't already
     /// present in the vector, according to the notion of contract equality defined in
     /// [crate::typecheck::eq].
-    pub fn push_elide(
+    pub fn push_dedup(
         initial_env: &Environment,
         contracts: &mut Vec<RuntimeContract>,
         env1: &Environment,
         ctr: Self,
         env2: &Environment,
     ) {
-        // eprintln!("push_elide: ({})", ctr.contract);
         let envs1 = EvalEnvs {
             eval_env: env1,
             initial_env,
         };
 
         for c in contracts.iter() {
-            // eprintln!("- comparing against ({})", c.contract);
             let envs = EvalEnvs {
                 eval_env: env2,
                 initial_env,
             };
             if contract_eq::<EvalEnvs>(0, &c.contract, envs1, &ctr.contract, envs) {
-                // eprintln!("  -> found equal contract, eliding");
                 return;
             }
         }
@@ -610,10 +607,15 @@ impl TypeAnnotation {
         self.typ.is_none() && self.contracts.is_empty()
     }
 
+    /// **Warning**: the contract equality check used in this function behaves like syntactic
+    /// equality, and doesn't take the environment into account. It's unsound for execution (it
+    /// could equate contracts that are actually totally distinct), but we use it only to trim
+    /// accumulated contracts before pretty-printing. Do not use prior to any form of evaluation.
+    ///
     /// Same as [`Combine::combine`], but eliminate duplicate contracts. As there's no notion of
-    /// environment when combining annotations, we use an unsound contract equality checking, which
-    /// just compares things syntactically.
-    pub fn combine_elide(left: Self, right: Self) -> Self {
+    /// environment when considering mere annotations, we use an unsound contract equality checking
+    /// which correspond to compares contracts syntactically.
+    pub fn combine_dedup(left: Self, right: Self) -> Self {
         let mut contracts = left.contracts;
 
         let typ = match (left.typ, right.typ) {