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, 6 insertions, 6 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 24f3b7726..05c64521a 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -45,7 +45,7 @@ type clausenv = {
   templtyp : constr freelisted }
 
 let cl_env ce = ce.env
-let cl_sigma ce = evars_of ce.evd
+let cl_sigma ce =  ce.evd
 
 let subst_clenv sub clenv = 
   { templval = map_fl (subst_mps sub) clenv.templval;
@@ -129,7 +129,7 @@ let clenv_conv_leq env sigma t c bound =
   let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
   let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
   let evars,_ = Evarconv.consider_remaining_unif_problems env evars in
-  let args = List.map (whd_evar (Evd.evars_of evars)) args in
+  let args = List.map (whd_evar ( evars)) args in
   check_evars env sigma evars (applist (c,args));
   args
 
@@ -254,7 +254,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
 let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
-  if isMeta (fst (whd_stack (evars_of clenv.evd) clenv.templtyp.rebus)) then
+  if isMeta (fst (whd_stack ( clenv.evd) clenv.templtyp.rebus)) then
     clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl)
       (clenv_unify_meta_types ~flags:flags clenv)
   else
@@ -341,7 +341,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv
     { templval = clenv.templval;
       templtyp = clenv.templtyp;
       evd = 
-        evar_merge (meta_merge clenv.evd nextclenv.evd) (evars_of clenv.evd);
+        evar_merge (meta_merge clenv.evd nextclenv.evd) ( clenv.evd);
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
@@ -402,7 +402,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (whd_stack (evars_of clenv.evd) u)) then
+  if isMeta (fst (whd_stack ( clenv.evd) u)) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -416,7 +416,7 @@ let clenv_unify_binding_type clenv c t u =
 let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
-  let c_typ = nf_betaiota (evars_of clenv'.evd) (clenv_get_type_of clenv' c) in
+  let c_typ = nf_betaiota ( clenv'.evd) (clenv_get_type_of clenv' c) in
   let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }