Tracking memory misallocation by trying to improve sharing.

1 files changed, 4 insertions, 3 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 93d9552c0d..264172d0c9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -487,10 +487,11 @@ let clear_hyps_in_evi evdref hyps concl ids =
   let nconcl =
     check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in
   let nhyps =
-    let check_context (id,ob,c) =
+    let check_context ((id,ob,c) as decl) =
       let err = OccurHypInSimpleClause (Some id) in
-      (id, Option.map (check_and_clear_in_constr evdref err ids) ob,
-	check_and_clear_in_constr evdref err ids c)
+      let ob' = Option.smartmap (fun c -> check_and_clear_in_constr evdref err ids c) ob in
+      let c' = check_and_clear_in_constr evdref err ids c in
+      if ob == ob' && c == c' then decl else (id, ob', c')
     in
     let check_value vk =
       match !vk with