Correction du bug #1754

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10458 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 91 insertions, 15 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e8d79703a..d653ed946 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -443,7 +443,15 @@ let do_restrict_hyps evd evk filter =
 
 exception Dependency_error of identifier
 
-let rec check_and_clear_in_constr evdref c ids =
+module EvkOrd = 
+struct
+  type t = Term.existential_key
+  let compare = Pervasives.compare
+end
+
+module EvkSet = Set.Make(EvkOrd)
+
+let rec check_and_clear_in_constr evdref c ids hist =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
      evars *)
@@ -453,24 +461,36 @@ let rec check_and_clear_in_constr evdref c ids =
   in 
     match kind_of_term c with
       | ( Rel _ | Meta _ | Sort _ ) -> c
+
       | ( Const _ | Ind _ | Construct _ ) -> 
 	  let vars = Environ.vars_of_global (Global.env()) c in
 	    List.iter check vars; c
+
       | Var id' ->  
 	  check id'; mkVar id'
+
       | Evar (evk,l as ev) -> 
 	  if Evd.is_defined_evar !evdref ev then
 	    (* If evk is already defined we replace it by its definition *)
 	    let nc = nf_evar (evars_of !evdref) c in 
-	      (check_and_clear_in_constr evdref nc ids)
-	  else
+	      (check_and_clear_in_constr evdref nc ids hist)
+	  else if EvkSet.mem evk hist then
+	    (* Loop detection => do nothing *)
+	    c
+	  else 
 	    (* We check for dependencies to elements of ids in the
 	       evar_info corresponding to e and in the instance of
 	       arguments. Concurrently, we build a new evar
 	       corresponding to e where hypotheses of ids have been
 	       removed *)
 	    let evi = Evd.find (evars_of !evdref) evk in
-	    let nconcl = check_and_clear_in_constr evdref (evar_concl evi) ids in
+	    let nconcl = check_and_clear_in_constr evdref (evar_concl evi) ids (EvkSet.add evk hist) in
+	    let ctxt,_ = List.fold_right 
+	      (fun b (hd,tl) ->
+		match tl with
+		  | [] -> assert false
+		  | x::tl' -> if b then (x::hd, tl') else (hd,tl'))
+	      (Evd.evar_filter evi) ([], List.rev (Evd.evar_context evi)) in
 	    let (nhyps,nargs) = 
 	      List.fold_right2 
 		(fun (id,ob,c) i (hy,ar) ->
@@ -478,26 +498,25 @@ let rec check_and_clear_in_constr evdref c ids =
 		    (hy,ar)
 		  else
 		    let d' = (id,
-			     (match ob with 
-				 None -> None
-			       | Some b -> Some (check_and_clear_in_constr evdref b ids)),
-			     check_and_clear_in_constr evdref c ids) in
-		    let i' = check_and_clear_in_constr evdref i ids in
+			     Option.map (fun b -> check_and_clear_in_constr evdref b ids (EvkSet.add evk hist)) ob,
+			     check_and_clear_in_constr evdref c ids (EvkSet.add evk hist)) in
+		    let i' = check_and_clear_in_constr evdref i ids (EvkSet.add evk hist) in
 		      (d'::hy, i'::ar)
 		) 	      
-		(evar_context evi) (Array.to_list l) ([],[]) in
+		ctxt (Array.to_list l) ([],[]) in
 	    let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
 	    let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
 	      evdref := Evd.evar_define evk ev' !evdref;
 	      let (evk',_) = destEvar ev' in
 		mkEvar(evk', Array.of_list nargs)
-      | _ -> map_constr (fun c -> check_and_clear_in_constr evdref c ids) c
+
+      | _ -> map_constr (fun c -> check_and_clear_in_constr evdref c ids hist) c
 
 and clear_hyps_in_evi evdref evi ids =
   (* clear_evar_hyps erases hypotheses ids in evi, 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 = try check_and_clear_in_constr evdref (evar_concl evi) ids 
+  let nconcl = try check_and_clear_in_constr evdref (evar_concl evi) ids EvkSet.empty
     with Dependency_error id' -> error (string_of_id id' ^ " is used in conclusion") in
   let (nhyps,_) = 
     let check_context (id,ob,c) = 
@@ -505,8 +524,8 @@ and clear_hyps_in_evi evdref evi ids =
 	(id,
 	(match ob with 
 	    None -> None
-	  | Some b -> Some (check_and_clear_in_constr evdref b ids)),
-	check_and_clear_in_constr evdref c ids)
+	  | Some b -> Some (check_and_clear_in_constr evdref b ids EvkSet.empty)),
+	check_and_clear_in_constr evdref c ids EvkSet.empty)
       with Dependency_error id' -> error (string_of_id id' ^ " is used in hypothesis "
 					   ^ string_of_id id) 
     in
diff --git a/test-suite/bugs/opened/shouldnotfail/1754.v b/test-suite/bugs/opened/shouldnotfail/1754.v
index 768d9c990..06b8dce85 100644
--- a/test-suite/bugs/opened/shouldnotfail/1754.v
+++ b/test-suite/bugs/opened/shouldnotfail/1754.v
@@ -20,5 +20,5 @@ Proof.
   3:intros h'' Hp''; econstructor; apply Hp''.
   3:intros h'' Hp''; apply Hp''.
   2:apply Hp'.
-  try clear H.
+  clear H.
 Admitted.
diff --git a/test-suite/bugs/opened/shouldnotfail/1774.v b/test-suite/bugs/opened/shouldnotfail/1774.v
new file mode 100644
index 000000000..4c24b481b
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/1774.v
@@ -0,0 +1,18 @@
+Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop).
+Axiom plImp : forall k P Q,
+  pl P Q k -> forall (P':nat -> Prop),
+    (forall k', P k' -> P' k') -> forall (Q':nat -> Prop),
+      (forall k', Q k' -> Q' k') ->
+      pl P' Q' k.
+
+Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
+  fun k' => exists k, P k k'.
+
+Goal forall k (A:nat -> nat -> Prop) (B:nat -> Prop),
+  pl (nexists A) B k.
+intros.
+eapply plImp.
+2:intros m' M'; econstructor; apply M'.
+2:intros m' M'; apply M'.
+simpl.
+Admitted.
diff --git a/test-suite/bugs/opened/shouldnotfail/1775.v b/test-suite/bugs/opened/shouldnotfail/1775.v
new file mode 100644
index 000000000..dab4120b9
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/1775.v
@@ -0,0 +1,39 @@
+Axiom pair : nat -> nat -> nat -> Prop.
+Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop).
+Axiom plImp : forall k P Q,
+  pl P Q k -> forall (P':nat -> Prop),
+    (forall k', P k' -> P' k') -> forall (Q':nat -> Prop),
+      (forall k', Q k' -> Q' k') ->
+      pl P' Q' k.
+
+Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
+  fun k' => exists k, P k k'.
+
+Goal forall s k k' m,
+  (pl k' (nexists (fun w => (nexists (fun b => pl (pair w w)
+    (pl (pair s b)
+    (nexists (fun w0 => (nexists (fun a => pl (pair b w0)
+      (nexists (fun w1 => (nexists (fun c => pl 
+        (pair a w1) (pl (pair a c) k))))))))))))))) m.
+intros.
+eapply plImp; [ | eauto | intros ].
+2:econstructor.
+2:econstructor.
+2:eapply plImp; [ | eauto | intros ].
+3:eapply plImp; [ | eauto | intros ].
+4:econstructor.
+4:econstructor.
+4:eapply plImp; [ | eauto | intros ].
+5:econstructor.
+5:econstructor.
+5:eauto.
+4:eauto.
+3:eauto.
+2:eauto.
+
+assert (X := 1).
+clear X.   (* very slow! *)
+
+simpl.  (* exception Not_found *)
+
+Admitted.