Correction d'un bug dans check_and_clear_in_constr + simplification de

la gestion des erreurs dans clear_hyps.



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

3 files changed, 58 insertions, 57 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 1d0273260d..6f50dc93fe 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -308,68 +308,74 @@ let do_restrict_hyps env k evd ev args =
       mkEvar(evn,Array.of_list ncargs)
 	
 
-type ch_error_loc = 
-    | InGoal
-    | InHyps of identifier
-    | InEvar of existential_key
+exception Dependency_error of identifier
 	
-let rec check_and_clear_in_constr evd loc c ids =
+let rec check_and_clear_in_constr evd c ids =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
      evars *)
-  match kind_of_term c with
-    | ( Rel _ | Meta _ | Sort _ ) -> c
-    | ( Const _ | Ind _ | Construct _ ) -> 
-	let vars = Environ.vars_of_global (Global.env()) c in
-	let check id' = 
-	  if List.mem id' ids then
-	    match loc with
-		InGoal -> error (string_of_id id' ^ " is used in conclusion")
-              | InHyps id -> error (string_of_id id' ^ " is used in hypothesis "
-                                   ^ string_of_id id)
-	      | InEvar n -> error (string_of_id id' ^ " is used in "
-                                   ^ string_of_existential n)
-	in 
-	  List.iter check vars; c
-    | Var id' ->  
-	(if List.mem id' ids then
-	    match loc with
-		InGoal -> error (string_of_id id' ^ " is used in conclusion")
-              | InHyps id -> error (string_of_id id' ^ " is used in hypothesis "
-                                    ^ string_of_id id)
-	      | InEvar n -> error (string_of_id id' ^ " is used in "
-                                    ^ string_of_existential n));
-	mkVar id'
-    | Evar (e,l) -> 
-	(* If e is already defined we replace it by its definition *)
-	if Evd.is_defined_evar !evd (e,l) then
-	  let nc = nf_evar (evars_of !evd) c in 
-	    (check_and_clear_in_constr evd loc nc ids)
-	else
-	  let evi = Evd.find (evars_of !evd) e in
-	  let evi' = clear_evar_hyps_in_evi evd (InEvar e) evi ids in
-	  let env = Sign.fold_named_context push_named (evar_context evi') ~init:(empty_env) in
-	  let ev'= e_new_evar evd env ~src:(evar_source e !evd) (evar_concl evi') in
-	    evd := Evd.evar_define e ev' !evd;
-	    ev'
-    | _ -> map_constr (fun c -> check_and_clear_in_constr evd loc c ids) c
-	
-and clear_evar_hyps_in_evi evd loc evi ids =
+  let check id' = 
+    if List.mem id' ids then
+      raise (Dependency_error id')
+  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 (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)
+	  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
+
+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 = check_and_clear_in_constr evd loc (evar_concl evi) ids in
+  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) = 
-      let loc' = match loc with
-	  InGoal -> InHyps id
-	| _ -> loc 
-      in
+      try
 	(id,
 	(match ob with 
 	    None -> None
-	  | Some b -> Some (check_and_clear_in_constr evd loc' b ids)),
-	check_and_clear_in_constr evd loc' 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
       remove_hyps ids aux (evar_hyps evi)
   in    
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index e8f3bf6f0c..767acf7258 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -162,9 +162,4 @@ val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
 
 (**********************************)
 (* Removing hyps in evars'context *)
-type ch_error_loc = 
-    | InGoal 
-    | InHyps of Names.identifier 
-    | InEvar of Term.existential_key
-
-val clear_evar_hyps_in_evi : evar_defs ref -> ch_error_loc -> evar_info -> identifier list -> evar_info
+val clear_hyps_in_evi : evar_defs ref -> evar_info -> identifier list -> evar_info
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 67e0ca1fe1..7c149e9647 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -71,7 +71,7 @@ let with_check = Options.with_option check
    forces the user to give them in order). *)
 let clear_hyps sigma ids gl =
   let evd = ref (Evd.create_evar_defs sigma) in
-  let ngl = Evarutil.clear_evar_hyps_in_evi evd InGoal gl ids in
+  let ngl = Evarutil.clear_hyps_in_evi evd gl ids in
     (ngl, evars_of !evd)
 
 (* The ClearBody tactic *)