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

5 files changed, 31 insertions, 31 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 8a9646a17..520f9b631 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -53,15 +53,15 @@ let subst_evar_in_evm evar def evm =
  * T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated
  * by this definition. *)
 
-let rec safe_evar_define evm ev c =
+let rec safe_define evm ev c =
   if not (closedn (-1) c) then raise Termops.CannotFilter else
-(*  msgnl(str"safe_evar_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*)
+(*  msgnl(str"safe_define "++pr_evar_defs evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*)
   let evi = (Evd.find evm ev) in
   let define_subst evm sigma =
     Util.Intmap.fold
       ( fun ev (e,c) evm -> 
 	  match kind_of_term c with Evar (i,_) when i=ev -> evm | _ ->
-	    safe_evar_define evm ev (lift (-List.length e) c)
+	    safe_define evm ev (lift (-List.length e) c)
       ) sigma evm in
   match evi.evar_body with
     | Evd.Evar_defined def ->
@@ -70,7 +70,7 @@ let rec safe_evar_define evm ev c =
 	let t = Libtypes.reduce (Typing.type_of (Global.env()) evm c) in
 	let u = Libtypes.reduce (evar_concl evi) in
 	let evm = subst_evar_in_evm ev c evm in
-	define_subst (Evd.define evm ev c) (Termops.filtering [] Reduction.CUMUL t u)
+	define_subst (Evd.define ev c evm) (Termops.filtering [] Reduction.CUMUL t u)
 
 let add_gen_ctx (cl,gen,evm) ctx : signature * constr list = 
   let rec really_new_evar () =
@@ -111,9 +111,9 @@ let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) =
 	let def = applistc (Libnames.constr_of_global gr) argl in
 (*	msgnl(str"essayons  ?"++Util.pr_int ev++spc()++str":="++spc()
 	      ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*)
-	(*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*)
+	(*++spc()++str"dans"++spc()++pr_evar_defs evm++spc());*)
 	try
- 	  let evm = safe_evar_define evm ev def in
+ 	  let evm = safe_define evm ev def in
 	  k (cl,gen,evm);
 	  if sort_is_prop && SubstSet.mem s !substs then raise Exit;
 	  substs := SubstSet.add s !substs
@@ -147,10 +147,10 @@ let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit
 	let tyl = List.map (fun (_,_,t) -> t) ctx in
 	let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in
 	let def = applistc c argl in	
-(*	msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*)
+(*	msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_defs evm);*)
 	try
 	  if not (Evd.is_defined evm ev) then
-	    let evm = safe_evar_define evm ev def in
+	    let evm = safe_define evm ev def in
 	    aux evm; k (cl,gen,evm)
 	with Termops.CannotFilter -> ()
     ) evl in
@@ -220,7 +220,7 @@ let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature
     ( fun ctx typ -> 
 	List.iter
 	  (fun ((cl,ev,evm),_,_) -> 
-(*	     msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*)
+(*	     msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_defs evm);*)
 	     smap := Gmapl.add (cl,evm) (ctx,ev) !smap)
 	  (Recordops.methods_matching typ)
     ) [] deftyp;
@@ -263,7 +263,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit)
        then Evd.remove evm ev,gen 
        else evm,(ev::gen))
     gen (evm,[]) in
-(*  msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*)
+(*  msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_defs evm);*)
   let ngen = List.length gen in
   let (_,ctx,evm) = List.fold_left
     ( fun (i,ctx,evm) ev -> 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 081d18292..b6c664020 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -72,7 +72,7 @@ type binder_list = (identifier located * bool * constr_expr) list
 (* Calls to interpretation functions. *)
 
 let interp_type_evars evdref env ?(impls=([],[])) typ =
-  let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
+  let typ' = intern_gen true ~impls ( !evdref) env typ in
   let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ'
     
@@ -133,7 +133,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
 let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
     ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
   let env = Global.env() in
-  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let isevars = ref Evd.empty in
   let tclass = 
     match bk with
     | Implicit ->
@@ -169,7 +169,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
   let env' = push_rel_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   isevars := resolve_typeclasses env !isevars;
-  let sigma = Evd.evars_of !isevars in
+  let sigma =  !isevars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
     if Lib.is_modtype () then
       begin
@@ -234,9 +234,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	let term = Termops.it_mkLambda_or_LetIn app ctx' in
 	isevars := Evarutil.nf_evar_defs !isevars;
 	let term = Evarutil.nf_isevar !isevars term in
-	let evm = Evd.evars_of (undefined_evars !isevars) in
+	let evm =  (undefined_evars !isevars) in
 	Evarutil.check_evars env Evd.empty !isevars termtype;
-	  if evm = Evd.empty then
+	  if Evd.is_empty evm then
 	    declare_instance_constant k pri global imps ?hook id term termtype
 	  else begin
 	    isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !isevars;
@@ -246,7 +246,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 		  (fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst
 		    | _ -> assert false);
 		if props <> [] then 
-		  Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
+		  Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS ( !isevars)) *)
 		    (!refine_ref (evm, term));
 		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
 	      Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
@@ -266,9 +266,9 @@ let named_of_rel_context l =
 
 let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
-  let evars = ref (Evd.create_evar_defs Evd.empty) in
+  let evars = ref Evd.empty in
   let (env', fullctx), impls = interp_context_evars evars env l in
-  let fullctx = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) fullctx in
+  let fullctx = Evarutil.nf_rel_context_evar ( !evars) fullctx in
   let ce t = Evarutil.check_evars env Evd.empty !evars t in
   List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
   let ctx = try named_of_rel_context fullctx with _ -> 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1ab819a5e..50c78d0ed 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -115,7 +115,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
     | Some comtyp ->
 	let ty = generalize_constr_expr comtyp bl in
 	let b = abstract_constr_expr com bl in
-	let evdref = ref (Evd.create_evar_defs Evd.empty) in
+	let evdref = ref Evd.empty in
 	let ty, impls = interp_type_evars_impls ~evdref env ty in
 	let b, imps = interp_casted_constr_evars_impls ~evdref env b ty in
 	let body, typ = nf_isevar !evdref b, nf_isevar !evdref ty in
@@ -509,7 +509,7 @@ let check_all_names_different indl =
   if l <> [] then raise (InductiveError (SameNamesOverlap l))
 
 let mk_mltype_data evdref env assums arity indname =
-  let is_ml_type = is_sort env (evars_of !evdref) arity in
+  let is_ml_type = is_sort env ( !evdref) arity in
   (is_ml_type,indname,assums)
 
 let prepare_param = function
@@ -530,7 +530,7 @@ let interp_cstrs evdref env impls mldata arity ind =
 let interp_mutual paramsl indl notations finite = 
   check_all_names_different indl;
   let env0 = Global.env() in
-  let evdref = ref (Evd.create_evar_defs Evd.empty) in
+  let evdref = ref Evd.empty in
   let (env_params, ctx_params), userimpls = 
     interp_context_evars ~fail_anonymous:false evdref env0 paramsl 
   in
@@ -562,7 +562,7 @@ let interp_mutual paramsl indl notations finite =
   (* Instantiate evars and check all are resolved *)
   let evd,_ = consider_remaining_unif_problems env_params !evdref in
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in
-  let sigma = evars_of evd in
+  let sigma =  evd in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
   let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
   let arities = List.map (nf_evar sigma) arities in
@@ -846,12 +846,12 @@ let interp_recursive fixkind l boxed =
   let fixnames = List.map (fun fix -> fix.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
-  let evdref = ref (Evd.create_evar_defs Evd.empty) in
+  let evdref = ref Evd.empty in
   let fixctxs, fiximps =
     List.split (List.map (interp_fix_context evdref env) fixl) in
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
-  let fixtypes = List.map (nf_evar (evars_of !evdref)) fixtypes in
+  let fixtypes = List.map (nf_evar ( !evdref)) fixtypes in
   let env_rec = push_named_types env fixnames fixtypes in
 
   (* Get interpretation metadatas *)
@@ -867,8 +867,8 @@ let interp_recursive fixkind l boxed =
 
   (* Instantiate evars and check all are resolved *)
   let evd,_ = consider_remaining_unif_problems env_rec !evdref in
-  let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in
-  let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in
+  let fixdefs = List.map (nf_evar ( evd)) fixdefs in
+  let fixtypes = List.map (nf_evar ( evd)) fixtypes in
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
   List.iter (check_evars env_rec Evd.empty evd) fixdefs;
   List.iter (check_evars env Evd.empty evd) fixtypes;
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 42fc6d0fc..e8ca54c9c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -522,10 +522,10 @@ let pr_constraints printenv env evm =
 	  prlist_with_sep (fun () -> fnl ()) 
 	  (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l
     else
-      pr_evar_map evm
+      pr_evar_defs evm
       
 let explain_unsatisfiable_constraints env evd constr =
-  let evm = Evd.evars_of evd in
+  let evm =  evd in
   match constr with
   | None ->
       str"Unable to satisfy the following constraints:" ++ fnl() ++
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 10d4e5dc6..fe478f080 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -32,7 +32,7 @@ open Topconstr
 (********** definition d'un record (structure) **************)
 
 let interp_evars evdref env ?(impls=([],[])) k typ =
-  let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
+  let typ' = intern_gen true ~impls ( !evdref) env typ in
   let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
 
@@ -64,7 +64,7 @@ let binders_of_decls = List.map binder_of_decl
 
 let typecheck_params_and_fields id t ps nots fs =
   let env0 = Global.env () in
-  let evars = ref (Evd.create_evar_defs Evd.empty) in
+  let evars = ref Evd.empty in
   let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in
   let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
@@ -73,7 +73,7 @@ let typecheck_params_and_fields id t ps nots fs =
   in
   let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in
   let evars = Typeclasses.resolve_typeclasses env_ar evars in
-  let sigma = Evd.evars_of evars in
+  let sigma =  evars in
   let newps = Evarutil.nf_rel_context_evar sigma newps in
   let newfs = Evarutil.nf_rel_context_evar sigma newfs in
   let ce t = Evarutil.check_evars env0 Evd.empty evars t in