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

diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index ebbb5505f..5b76c9587 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -880,9 +880,9 @@ let interp_pats i isevar env impls pat sign recu =
 			  str "Error parsing pattern: unnexpected left-hand side")
   in
     isevar := nf_evar_defs !isevar;
-    (nf_rel_context_evar (Evd.evars_of !isevar) varsctx, 
-    nf_env_evar (Evd.evars_of !isevar) env',
-    rev_map (nf_evar (Evd.evars_of !isevar)) pats)
+    (nf_rel_context_evar ( !isevar) varsctx, 
+    nf_env_evar ( !isevar) env',
+    rev_map (nf_evar ( !isevar)) pats)
       
 let interp_eqn i isevar env impls sign arity recu (pats, rhs) =
   let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in
@@ -916,8 +916,8 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
   let isevar = ref (create_evar_defs Evd.empty) in
   let (env', sign), impls = interp_context_evars isevar env l in
   let arity = interp_type_evars isevar env' t in
-  let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
-  let arity = nf_evar (Evd.evars_of !isevar) arity in
+  let sign = nf_rel_context_evar ( !isevar) sign in
+  let arity = nf_evar ( !isevar) arity in
   let arity = 
     if with_comp then
       let compid = add_suffix i "_comp" in
@@ -942,11 +942,11 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
       Option.iter (Command.declare_interning_data data) nt;
       map (interp_eqn i isevar fixenv data sign arity None) eqs) ()
   in
-  let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
-  let arity = nf_evar (Evd.evars_of !isevar) arity in
+  let sign = nf_rel_context_evar ( !isevar) sign in
+  let arity = nf_evar ( !isevar) arity in
   let prob = (i, sign, arity) in
-  let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in
-  let fixdecls = nf_rel_context_evar (Evd.evars_of !isevar) fixdecls in
+  let fixenv = nf_env_evar ( !isevar) fixenv in
+  let fixdecls = nf_rel_context_evar ( !isevar) fixdecls in
     (*   let ce = check_evars fixenv Evd.empty !isevar in *)
     (*   List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; *)
   let is_recursive, env' =
@@ -966,7 +966,7 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
     else t, ty
   in
   let obls, t', ty' = 
-    Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 ~status t ty
+    Eterm.eterm_obligations env i !isevar ( undef) 0 ~status t ty
   in
     if is_recursive then
       ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] []