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

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d7da100abc..d185bd64ec 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -52,7 +52,7 @@ let eval_flexible_term env c =
   | _ -> assert false
 
 let evar_apprec env evd stack c =
-  let sigma = evars_of evd in
+  let sigma =  evd in
   let rec aux s =
     let (t,stack) = whd_betaiota_deltazeta_for_iota_state env sigma s in
     match kind_of_term t with
@@ -62,7 +62,7 @@ let evar_apprec env evd stack c =
   in aux (c, append_stack_list stack empty_stack)
 
 let apprec_nohdbeta env evd c =
-  match kind_of_term (fst (Reductionops.whd_stack (evars_of evd) c)) with
+  match kind_of_term (fst (Reductionops.whd_stack ( evd) c)) with
     | (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
     | _ -> c
 
@@ -158,7 +158,7 @@ let ise_array2 evd f v1 v2 =
   else (evd,false)
 
 let rec evar_conv_x env evd pbty term1 term2 = 
-  let sigma = evars_of evd in
+  let sigma =  evd in
   let term1 = whd_castappevar sigma term1 in
   let term2 = whd_castappevar sigma term2 in
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
@@ -166,7 +166,7 @@ let rec evar_conv_x env evd pbty term1 term2 =
      Note: incomplete heuristic... *)
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then
-      if is_fconv pbty env (evars_of evd) term1 term2 then
+      if is_fconv pbty env ( evd) term1 term2 then
         Some true
       else if is_ground_env evd env then Some false
       else None
@@ -222,7 +222,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  then
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
-	    let t2 = nf_evar (evars_of evd) (applist appr2) in
+	    let t2 = nf_evar ( evd) (applist appr2) in
 	    let t2 = solve_pattern_eqn env l1 t2 in
 	    solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
 	  else if
@@ -254,7 +254,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  then
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
-	    let t1 = nf_evar (evars_of evd) (applist appr1) in
+	    let t1 = nf_evar ( evd) (applist appr1) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
 	    solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
 	  else if
@@ -293,7 +293,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
              if the first argument is a beta-redex (expand a constant
              only if necessary) or the second argument is potentially
              usable as a canonical projection *)
-	  if isLambda flex1 or is_open_canonical_projection (evars_of i) appr2
+	  if isLambda flex1 or is_open_canonical_projection ( i) appr2
 	  then
 	    match eval_flexible_term env flex1 with
 	    | Some v1 ->
@@ -322,7 +322,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	then
 	  (* Miller-Pfenning's patterns unification *)
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
-	  let t2 = nf_evar (evars_of evd) (applist appr2) in
+	  let t2 = nf_evar ( evd) (applist appr2) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
 	  solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
 	else
@@ -337,7 +337,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	then
 	  (* Miller-Pfenning's patterns unification *)
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
-	  let t1 = nf_evar (evars_of evd) (applist appr1) in
+	  let t1 = nf_evar ( evd) (applist appr1) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
 	  solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
 	else
@@ -382,7 +382,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
-                 let c = nf_evar (evars_of i) c1 in
+                 let c = nf_evar ( i) c1 in
                  evar_conv_x (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
 	| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
@@ -390,8 +390,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
               ise_and i
                 [(fun i -> evar_conv_x env i CONV b1 b2);
                  (fun i ->
-                   let b = nf_evar (evars_of i) b1 in
-	           let t = nf_evar (evars_of i) t1 in
+                   let b = nf_evar ( i) b1 in
+	           let t = nf_evar ( i) t1 in
                    evar_conv_x (push_rel (na,Some b,t) env) i pbty c'1 c'2);
                  (fun i -> ise_list2 i
                      (fun i -> evar_conv_x env i CONV) l1 l2)]
@@ -414,7 +414,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
- 	         let c = nf_evar (evars_of i) c1 in
+ 	         let c = nf_evar ( i) c1 in
 	         evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)]
 
 	| Ind sp1, Ind sp2 ->
@@ -508,15 +508,15 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
 	solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
-  let evi = Evd.find (evars_of evd) evk in
+  let evi = Evd.find ( evd) evk in
   let subst = make_pure_subst evi args in
   let subst' = List.filter (fun (id,c) -> c = term) subst in
   if subst' = [] then error "Too complex unification problem." else
-  Evd.evar_define evk (mkVar (fst (List.hd subst'))) evd
+  Evd.define evk (mkVar (fst (List.hd subst'))) evd
 
 let apply_conversion_problem_heuristic env evd pbty t1 t2 =
-  let t1 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t1) in
-  let t2 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t2) in
+  let t1 = apprec_nohdbeta env evd (whd_castappevar ( evd) t1) in
+  let t2 = apprec_nohdbeta env evd (whd_castappevar ( evd) t2) in
   let (term1,l1 as appr1) = decompose_app t1 in
   let (term2,l2 as appr2) = decompose_app t2 in
   match kind_of_term term1, kind_of_term term2 with