From 8cb6251702b09186ca41c5ce67464b83ccfb3d16 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 13 Jun 2014 11:45:51 +0200
Subject: Fixing "clear" in internal_cut_replace: forbid dependencies in the
 name of replaced hypothesis.

---
 pretyping/evarutil.ml  | 18 ++++++++++++++----
 pretyping/evarutil.mli |  3 +++
 2 files changed, 17 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index dc8199ffe7..0a9b376980 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -491,12 +491,12 @@ let rec check_and_clear_in_constr evdref err ids c =
 
       | _ -> map_constr (check_and_clear_in_constr evdref err ids) c
 
-let clear_hyps_in_evi evdref hyps concl ids =
+let clear_hyps_in_evi_main evdref hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occuring in evi *)
-  let nconcl =
-    check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in
+  let terms =
+    List.map (check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids) terms in
   let nhyps =
     let check_context ((id,ob,c) as decl) =
       let err = OccurHypInSimpleClause (Some id) in
@@ -517,7 +517,17 @@ let clear_hyps_in_evi evdref hyps concl ids =
     in
       remove_hyps ids check_context check_value hyps
   in
-  (nhyps,nconcl)
+  (nhyps,terms)
+
+let clear_hyps_in_evi evdref hyps concl ids =
+  match clear_hyps_in_evi_main evdref hyps [concl] ids with
+  | (nhyps,[nconcl]) -> (nhyps,nconcl)
+  | _ -> assert false
+
+let clear_hyps2_in_evi evdref hyps t concl ids =
+  match clear_hyps_in_evi_main evdref hyps [t;concl] ids with
+  | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl)
+  | _ -> assert false
 
 (** The following functions return the set of evars immediately
     contained in the object, including defined evars *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index aa302bac6f..55171eb4c4 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -208,6 +208,9 @@ val cleared : bool Store.field
 val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
   Id.Set.t -> named_context_val * types
 
+val clear_hyps2_in_evi : evar_map ref -> named_context_val -> types -> types ->
+  Id.Set.t -> named_context_val * types * types
+
 val push_rel_context_to_named_context : Environ.env -> types ->
   named_context_val * types * constr list * constr list * (identifier*constr) list
 
-- 
cgit v1.2.3