Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)

- Correction bug des filtres dans define_evar_as_abstraction
- Nettoyage, documentation et réorganisations diverses



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

1 files changed, 13 insertions, 5 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 6d75dada67..c583a0b228 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -47,7 +47,12 @@ let evar_hyps evi = evi.evar_hyps
 let evar_context evi = named_context_of_val evi.evar_hyps
 let evar_body evi = evi.evar_body
 let evar_filter evi = evi.evar_filter
-let evar_env evd = Global.env_of_context evd.evar_hyps
+let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps
+let evar_filtered_context evi = 
+  snd (list_filter2 (fun b c -> b) (evar_filter evi,evar_context evi))
+let evar_env evi = 
+  List.fold_right push_named (evar_filtered_context evi)
+    (reset_context (Global.env()))
 
 let eq_evar_info ei1 ei2 =
   ei1 == ei2 || 
@@ -129,16 +134,14 @@ let existential_type sigma (n,args) =
     try find sigma n
     with Not_found ->
       anomaly ("Evar "^(string_of_existential n)^" was not declared") in
-  let hyps = evar_context info in
-  let _,hyps = list_filter2 (fun b c -> b) (evar_filter info,hyps) in
+  let hyps = evar_filtered_context info in
   instantiate_evar hyps info.evar_concl (Array.to_list args)
 
 exception NotInstantiatedEvar
 
 let existential_value sigma (n,args) =
   let info = find sigma n in
-  let hyps = evar_context info in
-  let _,hyps = list_filter2 (fun b c -> b) (evar_filter info,hyps) in
+  let hyps = evar_filtered_context info in
   match evar_body info with
     | Evar_defined c ->
 	instantiate_evar hyps c (Array.to_list args)
@@ -598,6 +601,11 @@ let subst_defined_metas bl c =
   in try Some (substrec c) with Not_found -> None
 
 (**********************************************************)
+(* Failure explanation *)
+
+type unsolvability_explanation = SeveralInstancesFound of int
+
+(**********************************************************)
 (* Pretty-printing *)
 
 let pr_meta_map mmap =