Fixing "clear" in internal_cut_replace: forbid dependencies in the

name of replaced hypothesis.

4 files changed, 34 insertions, 10 deletions

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
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index d5086df1a3..e1cbe4af08 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -104,8 +104,13 @@ let check_typability env sigma c =
 
 let clear_hyps sigma ids sign cl =
   let evdref = ref (Evd.create_goal_evar_defs sigma) in
-  let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
-  (hyps,concl, !evdref)
+  let (hyps,cl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
+  (hyps, cl, !evdref)
+
+let clear_hyps2 sigma ids sign t cl =
+  let evdref = ref (Evd.create_goal_evar_defs sigma) in
+  let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi evdref sign t cl ids in
+  (hyps, t, cl, !evdref)
 
 (* The ClearBody tactic *)
 
@@ -578,17 +583,17 @@ let prim_refiner r sigma goal =
 
     | Cut (b,replace,id,t) ->
         let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
-	let sign,cl,sigma =
+	let sign,t,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
-	    let sign,cl,sigma = clear_hyps sigma (Id.Set.singleton id) sign cl in
+	    let sign,t,cl,sigma = clear_hyps2 sigma (Id.Set.singleton id) sign t cl in
 	    move_hyp true false ([],(id,None,t),named_context_of_val sign)
 	      nexthyp,
-	      cl,sigma
+	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
 	      error ("Variable " ^ Id.to_string id ^ " is already declared.");
-	     push_named_context_val (id,None,t) sign,cl,sigma) in
+	     push_named_context_val (id,None,t) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
 	let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in
diff --git a/test-suite/bugs/closed/3284.v b/test-suite/bugs/closed/3284.v
index a942887ee9..34cd09c6f4 100644
--- a/test-suite/bugs/closed/3284.v
+++ b/test-suite/bugs/closed/3284.v
@@ -13,5 +13,11 @@ Proof.
   intros A B C f g x H.
   Fail apply @functional_extensionality_dep in H.
   Fail apply functional_extensionality_dep in H.
+  eapply functional_extensionality_dep in H.
+Abort.
+
+Goal forall A B C (f g : forall (x : A) (y : B x), C x y), forall x:A, (forall x y, f x y = g x y) -> True.
+Proof.
+  intros A B C f g x H.
   specialize (H x).
   apply functional_extensionality_dep in H.