Imported Upstream version 8.1.pl3+dfsgupstream/8.1.pl3+dfsg

1 files changed, 42 insertions, 37 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6896ca69..16059d94 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 9869 2007-05-29 11:07:04Z herbelin $ *)
+(* $Id: evarutil.ml 10374 2007-12-13 13:16:52Z notin $ *)
 
 open Util
 open Pp
@@ -331,7 +331,7 @@ let do_restrict_hyps env k evd ev args =
 
 exception Dependency_error of identifier
 	
-let rec check_and_clear_in_constr evd c ids =
+let rec check_and_clear_in_constr evd 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 *)
@@ -347,45 +347,50 @@ let rec check_and_clear_in_constr evd c ids =
       | Var id' ->  
 	  check id'; mkVar id'
       | Evar (e,l) -> 
-	  if Evd.is_defined_evar !evd (e,l) then
-	    (* If e is already defined we replace it by its definition *)
-	    let nc = nf_evar (evars_of !evd) c in 
-	      (check_and_clear_in_constr evd nc ids)
+	  if (List.mem e hist) then
+	    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 !evd) e in
-	    let nconcl = check_and_clear_in_constr evd (evar_concl evi) ids in
-	    let (nhyps,nargs) = 
-	      List.fold_right2 
-		(fun (id,ob,c) i (hy,ar) ->
-		  if List.mem id ids then
-		    (hy,ar)
-		  else
-		    let d' = (id,
-			     (match ob with 
-				 None -> None
-			       | Some b -> Some (check_and_clear_in_constr evd b ids)),
-			     check_and_clear_in_constr evd c ids) in
-		    let i' = check_and_clear_in_constr evd i ids in
-		      (d'::hy, i'::ar)
-		) 	      
-		(evar_context evi) (Array.to_list l) ([],[]) in
-	    let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
-	    let ev'= e_new_evar evd env ~src:(evar_source e !evd) nconcl in
-	      evd := Evd.evar_define e ev' !evd;
-	      let (e',_) = destEvar ev' in
-		mkEvar(e', Array.of_list nargs)
-      | _ -> map_constr (fun c -> check_and_clear_in_constr evd c ids) c
+	    begin
+	      if Evd.is_defined_evar !evd (e,l) then
+		(* If e is already defined we replace it by its definition *)
+		let nc = nf_evar (evars_of !evd) c in 
+		  (check_and_clear_in_constr evd nc ids hist)
+	      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 !evd) e in
+		let nconcl = check_and_clear_in_constr evd (evar_concl evi) ids (e::hist) in
+		let (nhyps,nargs) = 
+		  List.fold_right2 
+		    (fun (id,ob,c) i (hy,ar) ->
+		      if List.mem id ids then
+			(hy,ar)
+		      else
+			let d' = (id,
+				 (match ob with 
+				     None -> None
+				   | Some b -> Some (check_and_clear_in_constr evd b ids (e::hist))),
+				 check_and_clear_in_constr evd c ids (e::hist)) in
+			let i' = check_and_clear_in_constr evd i ids (e::hist) in
+			  (d'::hy, i'::ar)
+		    ) 	      
+		    (evar_context evi) (Array.to_list l) ([],[]) in
+		let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
+		let ev'= e_new_evar evd env ~src:(evar_source e !evd) nconcl in
+		  evd := Evd.evar_define e ev' !evd;
+		  let (e',_) = destEvar ev' in
+		    mkEvar(e', Array.of_list nargs)
+	    end
+      | _ -> map_constr (fun c -> check_and_clear_in_constr evd c ids hist) c
 
 and clear_hyps_in_evi evd 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 evd (evar_concl evi) ids 
+  let nconcl = try check_and_clear_in_constr evd (evar_concl evi) ids []
     with Dependency_error id' -> error (string_of_id id' ^ " is used in conclusion") in
   let (nhyps,_) = 
     let aux (id,ob,c) = 
@@ -393,8 +398,8 @@ and clear_hyps_in_evi evd evi ids =
 	(id,
 	(match ob with 
 	    None -> None
-	  | Some b -> Some (check_and_clear_in_constr evd b ids)),
-	check_and_clear_in_constr evd c ids)
+	  | Some b -> Some (check_and_clear_in_constr evd b ids [])),
+	check_and_clear_in_constr evd c ids [])
       with Dependency_error id' -> error (string_of_id id' ^ " is used in hypothesis "
 					   ^ string_of_id id)
     in