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

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 54421f96f8..4134f89b27 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -43,14 +43,14 @@ let abstract_scheme env c l lname_typ =
     lname_typ
 
 let abstract_list_all env evd typ c l =
-  let ctxt,_ = splay_prod_n env (evars_of evd) (List.length l) typ in
+  let ctxt,_ = splay_prod_n env ( evd) (List.length l) typ in
   let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in
   let p = abstract_scheme env c l_with_all_occs ctxt in 
   try 
-    if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p
+    if is_conv_leq env ( evd) (Typing.mtype_of env evd p) typ then p
     else error "abstract_list_all"
   with UserError _ | Type_errors.TypeError _ ->
-    error_cannot_find_well_typed_abstraction env (evars_of evd) p l
+    error_cannot_find_well_typed_abstraction env ( evd) p l
 
 (**)
 
@@ -431,14 +431,14 @@ let applyHead env evd n c  =
     if n = 0 then 
       (evd, c)
     else 
-      match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with
+      match kind_of_term (whd_betadeltaiota env ( evd) cty) with
         | Prod (_,c1,c2) ->
             let (evd',evar) = 
 	      Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in
 	    apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
 	| _ -> error "Apply_Head_Then"
   in 
-  apprec n c (Typing.type_of env (evars_of evd) c) evd
+  apprec n c (Typing.type_of env ( evd) c) evd
 
 let is_mimick_head f =
   match kind_of_term f with
@@ -468,7 +468,7 @@ let try_to_coerce env evd c cty tycon =
   let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
   let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in
   if b then
-    let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in
+    let evd' = Evd.map_metas_fvalue (nf_evar ( evd')) evd' in
     (evd',j'.uj_val)
   else
     error "Cannot solve unification constraints"
@@ -481,16 +481,16 @@ let w_coerce_to_type env evd c cty mvty =
     (* inh_conv_coerce_rigid_to should have reasoned modulo reduction 
        but there are cases where it though it was not rigid (like in
        fst (nat,nat)) and stops while it could have seen that it is rigid *)
-    let cty = Tacred.hnf_constr env (evars_of evd) cty in
+    let cty = Tacred.hnf_constr env ( evd) cty in
     try_to_coerce env evd c cty tycon
 
 let w_coerce env evd mv c =
-  let cty = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in
+  let cty = get_type_of_with_meta env ( evd) (metas_of evd) c in
   let mvty = Typing.meta_type evd mv in
   w_coerce_to_type env evd c cty mvty
 
 let unify_to_type env evd flags c u =
-  let sigma = evars_of evd in
+  let sigma =  evd in
   let c = refresh_universes c in
   let t = get_type_of_with_meta env sigma (metas_of evd) c in
   let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
@@ -518,7 +518,7 @@ let order_metas metas =
 
 let solve_simple_evar_eqn env evd ev rhs =
   let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in
-  if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs);
+  if not b then error_cannot_unify env ( evd) (mkEvar ev,rhs);
   let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in
   if not b then error "Cannot solve unification constraints";
   evd
@@ -534,16 +534,16 @@ let w_merge env with_types flags (metas,evars) evd =
     match evars with
     | ((evn,_ as ev),rhs)::evars' ->
     	if is_defined_evar evd ev then
-	  let v = Evd.existential_value (evars_of evd) ev in
+	  let v = Evd.existential_value ( evd) ev in
 	  let (metas',evars'') =
-	    unify_0 env (evars_of evd) topconv flags rhs v in
+	    unify_0 env ( evd) topconv flags rhs v in
 	  w_merge_rec evd (metas'@metas) (evars''@evars') eqns
     	else begin
           let rhs' = subst_meta_instances metas rhs in
           match kind_of_term rhs with
 	  | App (f,cl) when is_mimick_head f & occur_meta rhs' ->
 	      if occur_evar evn rhs' then
-                error_occur_check env (evars_of evd) evn rhs';
+                error_occur_check env ( evd) evn rhs';
 	      let evd' = mimick_evar evd flags f (Array.length cl) evn in
 	      w_merge_rec evd' metas evars eqns
           | _ ->
@@ -568,7 +568,7 @@ let w_merge env with_types flags (metas,evars) evd =
     	if meta_defined evd mv then
 	  let {rebus=c'},(status',_) = meta_fvalue evd mv in
           let (take_left,st,(metas',evars')) =
-	    merge_instances env (evars_of evd) flags status' status c' c
+	    merge_instances env ( evd) flags status' status c' c
 	  in
 	  let evd' = 
             if take_left then evd 
@@ -588,16 +588,16 @@ let w_merge env with_types flags (metas,evars) evd =
     | [] -> evd
 		
   and mimick_evar evd flags hdc nargs sp =
-    let ev = Evd.find (evars_of evd) sp in
+    let ev = Evd.find ( evd) sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (mc,ec) =
-      unify_0 sp_env (evars_of evd') Cumul flags
-        (Retyping.get_type_of_with_meta sp_env (evars_of evd') (metas_of evd') c) ev.evar_concl in
+      unify_0 sp_env ( evd') Cumul flags
+        (Retyping.get_type_of_with_meta sp_env ( evd') (metas_of evd') c) ev.evar_concl in
     let evd'' = w_merge_rec evd' mc ec [] in
-    if (evars_of evd') == (evars_of evd'')
-    then Evd.evar_define sp c evd''
-    else Evd.evar_define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in
+    if ( evd') == ( evd'')
+    then Evd.define sp c evd''
+    else Evd.define sp (Evarutil.nf_evar ( evd'') c) evd'' in
 
   (* merge constraints *)
   w_merge_rec evd (order_metas metas) evars []
@@ -617,9 +617,9 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
    types of metavars are unifiable with the types of their instances    *)
 
 let check_types env evd flags subst m n =
-  let sigma = evars_of evd in
+  let sigma =  evd in
   if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then
-    unify_0_with_initial_metas subst true env (evars_of evd) topconv 
+    unify_0_with_initial_metas subst true env ( evd) topconv 
       flags
       (Retyping.get_type_of_with_meta env sigma (metas_of evd) m)
       (Retyping.get_type_of_with_meta env sigma (metas_of evd) n)
@@ -630,7 +630,7 @@ let w_unify_core_0 env with_types cv_pb flags m n evd =
   let (mc1,evd') = retract_coercible_metas evd in
   let subst1 = check_types env evd flags (mc1,[]) m n in
   let subst2 =
-     unify_0_with_initial_metas subst1 true env (evars_of evd') cv_pb flags m n
+     unify_0_with_initial_metas subst1 true env ( evd') cv_pb flags m n
   in 
   w_merge env with_types flags subst2 evd'
 
@@ -743,8 +743,8 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
   w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd'
 
 let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
-  let c1, oplist1 = whd_stack (evars_of evd) ty1 in
-  let c2, oplist2 = whd_stack (evars_of evd) ty2 in
+  let c1, oplist1 = whd_stack ( evd) ty1 in
+  let c2, oplist2 = whd_stack ( evd) ty2 in
   match kind_of_term c1, kind_of_term c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
@@ -782,8 +782,8 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
    Meta(1) had meta-variables in it. *)
 let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
   let cv_pb = of_conv_pb cv_pb in
-  let hd1,l1 = whd_stack (evars_of evd) ty1 in
-  let hd2,l2 = whd_stack (evars_of evd) ty2 in
+  let hd1,l1 = whd_stack ( evd) ty1 in
+  let hd2,l2 = whd_stack ( evd) ty2 in
     match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
       (* Pattern case *)
       | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)