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

4 files changed, 10 insertions, 10 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 62518eaf7..8b7a7d99f 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -80,7 +80,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
     else clenv.evd
   in
   tclTHEN
-    (tclEVARS (evars_of evd')) 
+    (tclEVARS ( evd')) 
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
@@ -115,7 +115,7 @@ let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
   let env = pf_env gls in
   let evd = create_goal_evar_defs (project gls) in
   let evd' = w_unify false env CONV ~flags m n evd in
-  tclIDTAC {it = gls.it; sigma = evars_of evd'}
+  tclIDTAC {it = gls.it; sigma =  evd'}
 
 let unify ?(flags=fail_quick_unif_flags) m gls =
   let n = pf_concl gls in unifyTerms ~flags m n gls
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 17f63933f..e1236bbaa 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -23,20 +23,20 @@ open Refiner
 (* w_tactic pour instantiate *) 
 
 let w_refine evk rawc evd =
-  if Evd.is_defined (evars_of evd) evk then 
+  if Evd.is_defined ( evd) evk then 
     error "Instantiate called on already-defined evar";
-  let e_info = Evd.find (evars_of evd) evk in
+  let e_info = Evd.find ( evd) evk in
   let env = Evd.evar_env e_info in
   let sigma,typed_c =
     try Pretyping.Default.understand_tcc ~resolve_classes:false
-      (evars_of evd) env ~expected_type:e_info.evar_concl rawc
+      ( evd) env ~expected_type:e_info.evar_concl rawc
     with _ ->
       let loc = Rawterm.loc_of_rawconstr rawc in
       user_err_loc 
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
   in
-    evar_define evk typed_c (evars_reset_evd sigma evd)
+    define evk typed_c (evars_reset_evd sigma evd)
 
 (* vernac command Existential *)
 
@@ -56,4 +56,4 @@ let instantiate_pf_com n com pfts =
   let rawc = Constrintern.intern_constr sigma env com in 
   let evd = create_goal_evar_defs sigma in
   let evd' = w_refine evk rawc evd in
-    change_constraints_pftreestate (evars_of evd') pfts
+    change_constraints_pftreestate ( evd') pfts
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 7424685bc..5f164b020 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -99,7 +99,7 @@ let check_typability env sigma c =
 let clear_hyps sigma ids sign cl =
   let evdref = ref (Evd.create_goal_evar_defs sigma) in
   let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
-  (hyps,concl,evars_of !evdref)
+  (hyps,concl, !evdref)
 
 (* The ClearBody tactic *)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 19ea5c398..f9b7b8677 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -241,9 +241,9 @@ let rec pr_list f = function
   | a::l1 -> (f a) ++ pr_list f l1
 
 let pr_gls gls =
-  hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
+  hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
 
 let pr_glls glls =
-  hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
+  hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++
          prlist_with_sep pr_fnl db_pr_goal (sig_it glls))