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

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index ece3586a1..c22a16048 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -43,30 +43,30 @@ let inductive_type_knowing_parameters env ind jl =
 let rec execute env evd cstr =
   match kind_of_term cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = nf_evar (evars_of evd) (meta_type evd n) }
+        { uj_val = cstr; uj_type = nf_evar ( evd) (meta_type evd n) }
 
     | Evar ev ->
-        let sigma = Evd.evars_of evd in
+        let sigma =  evd in
 	let ty = Evd.existential_type sigma ev in
-	let jty = execute env evd (nf_evar (evars_of evd) ty) in
+	let jty = execute env evd (nf_evar ( evd) ty) in
 	let jty = assumption_of_judgment env jty in
 	{ uj_val = cstr; uj_type = jty }
 	
     | Rel n -> 
-	j_nf_evar (evars_of evd) (judge_of_relative env n)
+	j_nf_evar ( evd) (judge_of_relative env n)
 
     | Var id -> 
-        j_nf_evar (evars_of evd) (judge_of_variable env id)
+        j_nf_evar ( evd) (judge_of_variable env id)
 	  
     | Const c ->
-        make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c))
+        make_judge cstr (nf_evar ( evd) (type_of_constant env c))
 	  
     | Ind ind ->
-	make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind))
+	make_judge cstr (nf_evar ( evd) (type_of_inductive env ind))
 	  
     | Construct cstruct -> 
 	make_judge cstr
-          (nf_evar (evars_of evd) (type_of_constructor env cstruct))
+          (nf_evar ( evd) (type_of_constructor env cstruct))
 
     | Case (ci,p,c,lf) ->
         let cj = execute env evd c in
@@ -101,12 +101,12 @@ let rec execute env evd cstr =
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (inductive_type_knowing_parameters env ind
-		    (jv_nf_evar (evars_of evd) jl))
+		    (jv_nf_evar ( evd) jl))
 	    | Const cst -> 
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (constant_type_knowing_parameters env cst
-		    (jv_nf_evar (evars_of evd) jl))
+		    (jv_nf_evar ( evd) jl))
 	    | _ -> 
 		execute env evd f
 	in
@@ -157,7 +157,7 @@ and execute_array env evd = Array.map (execute env evd)
 and execute_list env evd = List.map (execute env evd)
 
 let mcheck env evd c t =
-  let sigma = Evd.evars_of evd in
+  let sigma =  evd in
   let j = execute env evd (nf_evar sigma c) in
   if not (is_conv_leq env sigma j.uj_type t) then
     error_actual_type env j (nf_evar sigma t)
@@ -165,13 +165,13 @@ let mcheck env evd c t =
 (* Type of a constr *)
  
 let mtype_of env evd c =
-  let j = execute env evd (nf_evar (evars_of evd) c) in
+  let j = execute env evd (nf_evar ( evd) c) in
   (* We are outside the kernel: we take fresh universes *)
   (* to avoid tactics and co to refresh universes themselves *)
   Termops.refresh_universes j.uj_type
 
 let msort_of env evd c =
-  let j = execute env evd (nf_evar (evars_of evd) c) in
+  let j = execute env evd (nf_evar ( evd) c) in
   let a = type_judgment env j in
   a.utj_type
 
@@ -185,5 +185,5 @@ let check env sigma c   =
 (* The typed type of a judgment. *)
 
 let mtype_of_type env evd constr =
-  let j = execute env evd (nf_evar (evars_of evd) constr) in
+  let j = execute env evd (nf_evar ( evd) constr) in
   assumption_of_judgment env j