On remplace evar_map par evar_defs (seul evar_defs est désormais exporté

par Evd). Ça s'accompagne de quelques autres modifications de 
l'interface (certaines fonctions étaient des doublons, ou des 
conversions entre evar_map et evar_defs).

J'ai modifié un peu la structure de evd.ml aussi, pour éviter des 
fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai 
introduit des sous-modules pour les différentes couches.

Il y a à l'heure actuelle une pénalité en performance assez sévère (due 
principalement à la nouvelle mouture de Evd.merge, si mon diagnostique 
est correct). Mais fera l'objet de plusieurs optimisations dans les 
commits à venir.

Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un 
appel de Decl_proof_instr.mark_as_done visiblement, je suis pour 
l'instant incapable de comprendre ce qui cause cette erreur. J'espère 
qu'on pourra le déterminer rapidement.

Ce commit est le tout premier commit dans le trunk en rapport avec les 
évolution futures de la machine de preuve, en vue en particulier 
d'obtenir un "vrai refine".



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

1 files changed, 14 insertions, 14 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 85e14d482..3a5f35125 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -123,7 +123,7 @@ module Default = struct
     with _ -> anomaly "apply_coercion"
 
   let inh_app_fun env evd j = 
-    let t = whd_betadeltaiota env (evars_of evd) j.uj_type in
+    let t = whd_betadeltaiota env ( evd) j.uj_type in
       match kind_of_term t with
 	| Prod (_,_,_) -> (evd,j)
 	| Evar ev ->
@@ -132,21 +132,21 @@ module Default = struct
 	| _ ->
        	    (try
       	       let t,p =
-		 lookup_path_to_fun_from env (evars_of evd) j.uj_type in
-		 (evd,apply_coercion env (evars_of evd) p j t)
+		 lookup_path_to_fun_from env ( evd) j.uj_type in
+		 (evd,apply_coercion env ( evd) p j t)
 	     with Not_found -> (evd,j))
 
   let inh_tosort_force loc env evd j =
     try
-      let t,p = lookup_path_to_sort_from env (evars_of evd) j.uj_type in
-      let j1 = apply_coercion env (evars_of evd) p j t in 
-      let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in
+      let t,p = lookup_path_to_sort_from env ( evd) j.uj_type in
+      let j1 = apply_coercion env ( evd) p j t in 
+      let j2 = on_judgment_type (whd_evar ( evd)) j1 in
         (evd,type_judgment env j2)
     with Not_found ->
-      error_not_a_type_loc loc env (evars_of evd) j
+      error_not_a_type_loc loc env ( evd) j
 
   let inh_coerce_to_sort loc env evd j =
-    let typ = whd_betadeltaiota env (evars_of evd) j.uj_type in
+    let typ = whd_betadeltaiota env ( evd) j.uj_type in
       match kind_of_term typ with
 	| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
 	| Evar ev when not (is_defined_evar evd ev) ->
@@ -166,11 +166,11 @@ module Default = struct
     else
     let v', t' =
       try 
-	let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in
+	let t2,t1,p = lookup_path_between env ( evd) (t,c1) in
 	  match v with
 	      Some v -> 
 		let j =
-		  apply_coercion env (evars_of evd) p
+		  apply_coercion env ( evd) p
 		    {uj_val = v; uj_type = t} t2 in
 		  Some j.uj_val, j.uj_type
 	    | None -> None, t
@@ -185,8 +185,8 @@ module Default = struct
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
     match
-      kind_of_term (whd_betadeltaiota env (evars_of evd) t),
-      kind_of_term (whd_betadeltaiota env (evars_of evd) c1)
+      kind_of_term (whd_betadeltaiota env ( evd) t),
+      kind_of_term (whd_betadeltaiota env ( evd) c1)
     with
     | Prod (name,t1,t2), Prod (_,u1,u2) -> 
         (* Conversion did not work, we may succeed with a coercion. *)
@@ -215,7 +215,7 @@ module Default = struct
 	    try 
 	      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
 	    with NoCoercion ->
-	      let sigma = evars_of evd in
+	      let sigma =  evd in
 		error_actual_type_loc loc env sigma cj t
 	  in
 	  let val' = match val' with Some v -> v | None -> assert(false) in
@@ -253,7 +253,7 @@ module Default = struct
 		  pi1 (inh_conv_coerce_to_fail loc env' evd None t t')
 		with NoCoercion ->
 		  evd) (* Maybe not enough information to unify *)
-	      (*let sigma = evars_of evd in
+	      (*let sigma =  evd in
 		error_cannot_coerce env' sigma (t, t'))*)
 	    else evd
 	with Invalid_argument _ -> evd	  *)