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

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 9d8b6c3b57..672c3d21cc 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -390,7 +390,7 @@ let valid goals p res_sigma l =
       (fun sigma (ev, evi) prf ->
 	let cstr, obls = Refiner.extract_open_proof !res_sigma prf in
 	  if not (Evd.is_defined sigma ev) then
-	    Evd.define sigma ev cstr
+	    Evd.define ev cstr sigma
 	  else sigma)
       !res_sigma goals l
   in raise (Found evm)
@@ -402,7 +402,7 @@ let is_dependent ev evm =
     evm false
     
 let resolve_all_evars_once debug (mode, depth) env p evd =
-  let evm = Evd.evars_of evd in
+  let evm =  evd in
   let goals, evm' = 
     Evd.fold
       (fun ev evi (gls, evm') ->
@@ -438,7 +438,7 @@ let has_undefined p oevd evd =
   Evd.fold (fun ev evi has -> has ||
     (evi.evar_body = Evar_empty && p ev evi && 
 	(try Typeclasses.is_resolvable (Evd.find oevd ev) with _ -> true)))
-    (Evd.evars_of evd) false
+    ( evd) false
 
 let rec merge_deps deps = function
   | [] -> [deps]
@@ -459,8 +459,8 @@ let select_evars evs evm =
     evm Evd.empty
 
 let resolve_all_evars debug m env p oevd do_split fail =
-  let oevm = Evd.evars_of oevd in
-  let split = if do_split then split_evars (Evd.evars_of (Evd.undefined_evars oevd)) else [Intset.empty] in
+  let oevm =  oevd in
+  let split = if do_split then split_evars ( (Evd.undefined_evars oevd)) else [Intset.empty] in
   let p = if do_split then 
     fun comp ev evi -> (Intset.mem ev comp || not (Evd.mem oevm ev)) && p ev evi
     else fun _ -> p 
@@ -481,7 +481,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
 	  | None -> 
 	      if fail then 
 		(* Unable to satisfy the constraints. *)
-		let evm = Evd.evars_of evd in
+		let evm =  evd in
 		let evm = if do_split then select_evars comp evm else evm in
 		let _, ev = Evd.fold 
 		  (fun ev evi (b,acc) -> 
@@ -615,9 +615,9 @@ let is_applied_setoid_relation t =
       let head = if isApp c then fst (destApp c) else c in 
 	if eq_constr (Lazy.force coq_eq) head then false
 	else (try      
-	    let evd, evar = Evarutil.new_evar (Evd.create_evar_defs Evd.empty) (Global.env()) (new_Type ()) in
+	    let evd, evar = Evarutil.new_evar Evd.empty (Global.env()) (new_Type ()) in
 	    let inst = mkApp (Lazy.force setoid_relation, [| evar; c |]) in
-	      ignore(Typeclasses.resolve_one_typeclass (Global.env()) (Evd.evars_of evd) inst);
+	      ignore(Typeclasses.resolve_one_typeclass (Global.env()) ( evd) inst);
 	      true
 	  with _ -> false)
   | _ -> false
@@ -645,19 +645,19 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
       | Some x -> f x
   in
   let rec aux env ty l =
-    let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) ty in
+    let t = Reductionops.whd_betadeltaiota env ( !isevars) ty in
       match kind_of_term t, l with
       | Prod (na, ty, b), obj :: cstrs -> 
 	  if dependent (mkRel 1) b then
 	    let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in
-	    let ty = Reductionops.nf_betaiota (Evd.evars_of !isevars) ty in
+	    let ty = Reductionops.nf_betaiota ( !isevars) ty in
 	    let pred = mkLambda (na, ty, b) in
 	    let liftarg = mkLambda (na, ty, arg) in
 	    let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
 	      mkProd(na, ty, b), arg', (ty, None) :: evars
 	  else
 	    let (b', arg, evars) = aux env (subst1 mkProp b) cstrs in
-	    let ty = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in
+	    let ty = Reductionops.nf_betaiota( !isevars) ty in
 	    let relty = mk_relty ty obj in
 	    let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
 	      mkProd(na, ty, b), newarg, (ty, Some relty) :: evars
@@ -665,7 +665,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
       | _, [] -> 
 	  (match finalcstr with
 	      None -> 
-		let t = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in
+		let t = Reductionops.nf_betaiota( !isevars) ty in
 		let rel = mk_relty t None in 
 		  t, rel, [t, Some rel]
 	    | Some codom -> let (t, rel) = Lazy.force codom in
@@ -793,7 +793,7 @@ let rewrite2_unif_flags = {
 }
 
 let convertible env evd x y =
-  Reductionops.is_conv env (Evd.evars_of evd) x y
+  Reductionops.is_conv env ( evd) x y
   
 let allowK = true
 
@@ -803,7 +803,7 @@ let refresh_hypinfo env sigma hypinfo =
       match c with 
 	| Some c ->
 	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
-	    hypinfo := decompose_setoid_eqhyp env (Evd.evars_of cl.evd) c l2r;
+	    hypinfo := decompose_setoid_eqhyp env ( cl.evd) c l2r;
 	| _ -> ()
   else ()
 
@@ -832,7 +832,7 @@ let unify_eqn env sigma hypinfo t =
 	      in
 	      let evd' = Typeclasses.resolve_typeclasses ~fail:false env'.env env'.evd in
 	      let env' = { env' with evd = evd' } in
-	      let nf c = Evarutil.nf_evar (Evd.evars_of evd') (Clenv.clenv_nf_meta env' c) in
+	      let nf c = Evarutil.nf_evar ( evd') (Clenv.clenv_nf_meta env' c) in
 	      let c1 = nf c1 and c2 = nf c2
 	      and car = nf car and rel = nf rel 
 	      and prf = nf (Clenv.clenv_value env') in
@@ -923,7 +923,7 @@ let build_new gl env sigma flags loccs hypinfo concl cstr evars =
       | Some (env', (prf, hypinfo as x)) when is_occ occ -> 
 	  begin 
 	    evars := Evd.evar_merge !evars 
-	      (Evd.evars_of (Evd.undefined_evars (Evarutil.nf_evar_defs env'.evd)));
+	      ( (Evd.undefined_evars (Evarutil.nf_evar_defs env'.evd)));
 	    match cstr with
 	    | None -> Some x, occ
 	    | Some _ ->
@@ -960,7 +960,7 @@ let build_new gl env sigma flags loccs hypinfo concl cstr evars =
 			let nargs = Array.length args in
 			let res = 
 			  mkApp (prf, args),
-			  (decomp_prod env (Evd.evars_of !evars) nargs car, 
+			  (decomp_prod env ( !evars) nargs car, 
 			  decomp_pointwise nargs rel, mkApp(c1, args), mkApp(c2, args))
 			in Some res, occ
 		else rewrite_args occ
@@ -1079,7 +1079,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
 			     [| mkMeta goal_meta; t |])))
 	  in
 	  let evartac =
-	    let evd = Evd.evars_of undef in
+	    let evd =  undef in
 	      if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd)
 	      else tclIDTAC
 	  in tclTHENLIST [evartac; rewtac] gl
@@ -1198,7 +1198,7 @@ END
 (*     let depth = match depth with Some i -> i | None -> default_eauto_depth in *)
 (*       match resolve_typeclass_evars d (mode, depth) env evd false with *)
 (*       | Some evd' ->  *)
-(* 	  let goal = Evd.find (Evd.evars_of evd') 1 in *)
+(* 	  let goal = Evd.find ( evd') 1 in *)
 (* 	    (match goal.evar_body with *)
 (* 	    | Evar_empty -> tclIDTAC gl *)
 (* 	    | Evar_defined b -> refine b gl) *)
@@ -1431,7 +1431,7 @@ let build_morphism_signature m =
   let env = Global.env () in
   let m = Constrintern.interp_constr Evd.empty env m in
   let t = Typing.type_of env Evd.empty m in
-  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let isevars = ref Evd.empty in
   let cstrs = 
     let rec aux t = 
       match kind_of_term t with
@@ -1459,7 +1459,7 @@ let build_morphism_signature m =
 	
 let default_morphism sign m =
   let env = Global.env () in
-  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let isevars = ref Evd.empty in
   let t = Typing.type_of env Evd.empty m in
   let _, sign, evars =
     build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel)
@@ -1578,7 +1578,7 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
     let mvs = clenv_dependent false cl' in
       clenv_pose_metas_as_evars cl' mvs
   in
-  let nf c = Evarutil.nf_evar (Evd.evars_of cl'.evd) (Clenv.clenv_nf_meta cl' c) in
+  let nf c = Evarutil.nf_evar ( cl'.evd) (Clenv.clenv_nf_meta cl' c) in
   let c1 = nf c1 and c2 = nf c2 and car = nf car and rel = nf rel in
   check_evar_map_of_evars_defs cl'.evd;
   let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in
@@ -1673,13 +1673,13 @@ let typeclass_app_constrexpr t ?(bindings=NoBindings) gl =
   let t', bl = Tacinterp.intern_constr_with_bindings gs (t,bindings) in
   let j = Pretyping.Default.understand_judgment_tcc evars env (fst t') in
   let bindings = Tacinterp.interp_bindings my_ist gl bl in
-    typeclass_app (Evd.evars_of !evars) gl ~bindings:bindings j.uj_val j.uj_type
+    typeclass_app ( !evars) gl ~bindings:bindings j.uj_val j.uj_type
 
 let typeclass_app_raw t gl =
   let env = pf_env gl in
   let evars = ref (create_evar_defs (project gl)) in
   let j = Pretyping.Default.understand_judgment_tcc evars env t in
-    typeclass_app (Evd.evars_of !evars) gl j.uj_val j.uj_type
+    typeclass_app ( !evars) gl j.uj_val j.uj_type
 
 let pr_gen prc _prlc _prtac c = prc c
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index dd9f648caa..0d81879843 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -566,7 +566,7 @@ exception NotDiscriminable
 let eq_baseid = id_of_string "e"
 
 let apply_on_clause (f,t) clause =
-  let sigma = Evd.evars_of clause.evd in
+  let sigma =  clause.evd in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
   let argmv = 
     (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
@@ -588,7 +588,7 @@ let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
     [onLastHyp gen_absurdity; refine pf]
 
 let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
-  let sigma = Evd.evars_of eq_clause.evd in
+  let sigma =  eq_clause.evd in
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
     | Inr _ ->
@@ -608,7 +608,7 @@ let onEquality with_evars tac (c,lbindc) gls =
     with PatternMatchingFailure ->
       errorlabstrm "" (str"No primitive equality found.") in
   tclTHEN
-    (Refiner.tclEVARS (Evd.evars_of eq_clause'.evd)) 
+    (Refiner.tclEVARS ( eq_clause'.evd)) 
     (tac eq eq_clause') gls
 
 let onNegatedEquality with_evars tac gls =
@@ -739,21 +739,21 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       else
 	error "Cannot solve an unification problem."
     else
-      let (a,p_i_minus_1) = match whd_beta_stack (evars_of !evdref) p_i with
+      let (a,p_i_minus_1) = match whd_beta_stack ( !evdref) p_i with
 	| (_sigS,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausal_form: should be a sigma type" in
       let ev = Evarutil.e_new_evar evdref env a in
       let rty = beta_applist(p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       match
-	Evd.existential_opt_value (Evd.evars_of !evdref) 
+	Evd.existential_opt_value ( !evdref) 
 	(destEvar ev)
       with
 	| Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
 	| None -> anomaly "Not enough components to build the dependent tuple"
   in
   let scf = sigrec_clausal_form siglen ty in
-  Evarutil.nf_evar (Evd.evars_of !evdref) scf
+  Evarutil.nf_evar ( !evdref) scf
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
@@ -891,7 +891,7 @@ exception Not_dep_pair
 
 
 let injEq ipats (eq,(t,t1,t2)) eq_clause =
-  let sigma = Evd.evars_of eq_clause.evd in
+  let sigma =  eq_clause.evd in
   let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
     | Inl _ ->
@@ -953,7 +953,7 @@ let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls
 
 let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls =
   let sort = pf_apply get_type_of gls (pf_concl gls) in 
-  let sigma = Evd.evars_of clause.evd in
+  let sigma =  clause.evd in
   let env = pf_env gls in 
   match find_positions env sigma t1 t2 with
     | Inl (cpath, (_,dirn), _) ->
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 5e87d432ba..d03b26192c 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -54,7 +54,7 @@ let instantiate n rawc ido gl =
     let ev,_ =  destEvar (List.nth evl (n-1)) in
     let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in
       tclTHEN
-        (tclEVARS (evars_of evd'))
+        (tclEVARS ( evd'))
         tclNORMEVAR
         gl
 	
@@ -74,6 +74,6 @@ let instantiate_tac = function
 let let_evar name typ gls =
   let evd = Evd.create_goal_evar_defs gls.sigma in
   let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in
-  Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd'))
+  Refiner.tclTHEN (Refiner.tclEVARS ( evd'))
     (Tactics.letin_tac None name evar None nowhere) gls
  
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9ca68c9a18..0129c06c87 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1427,14 +1427,14 @@ let solvable_by_tactic env evi (ev,args) src =
 let solve_remaining_evars env initial_sigma evd c =
   let evdref = ref (Typeclasses.resolve_typeclasses ~fail:true env evd) in
   let rec proc_rec c =
-    match kind_of_term (Reductionops.whd_evar (evars_of !evdref) c) with
+    match kind_of_term (Reductionops.whd_evar ( !evdref) c) with
       | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
             let (loc,src) = evar_source ev !evdref in
-	    let sigma = evars_of !evdref in
+	    let sigma =  !evdref in
 	    let evi = Evd.find sigma ev in
 	    (try 
 	      let c = solvable_by_tactic env evi k src in
-	      evdref := Evd.evar_define ev c !evdref;
+	      evdref := Evd.define ev c !evdref;
 	      c
 	    with Exit ->
 	      Pretype_errors.error_unsolvable_implicit loc env sigma evi src None)
@@ -1466,11 +1466,11 @@ let interp_econstr kind ist sigma env cc =
 (* Interprets an open constr *)
 let interp_open_constr ccl ist sigma env cc =
   let evd,c = interp_gen (OfType ccl) ist sigma env cc in
-  (evars_of evd,c)
+  ( evd,c)
 
 let interp_open_type ccl ist sigma env cc =
   let evd,c = interp_gen IsType ist sigma env cc in
-  (evars_of evd,c)
+  ( evd,c)
 
 let interp_constr = interp_econstr (OfType None)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0bcdcc8fd4..b45861fd33 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -528,7 +528,7 @@ let resolve_classes gl =
     if evd = Evd.empty then tclIDTAC gl
     else
       let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in
-	(tclTHEN (tclEVARS (Evd.evars_of evd')) tclNORMEVAR) gl
+	(tclTHEN (tclEVARS ( evd')) tclNORMEVAR) gl
 
 (**************************)
 (*     Cut tactics        *)
@@ -577,7 +577,7 @@ let clenv_refine_in with_evars ?(with_classes=true) id clenv gl =
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
   tclTHEN
-    (tclEVARS (evars_of clenv.evd))
+    (tclEVARS ( clenv.evd))
     (cut_replacing id new_hyp_typ
       (fun x gl -> refine_no_check new_hyp_prf gl)) gl
 
@@ -747,7 +747,7 @@ let check_evars sigma evm gl =
   in 
   if rest <> Evd.empty then
     errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ 
-      fnl () ++ pr_evar_map rest)
+      fnl () ++ pr_evar_defs rest)
 
 let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
   let flags = 
@@ -985,7 +985,7 @@ let specialize mopt (c,lbind) g =
       let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
       let clause = clenv_unify_meta_types clause in
       let (thd,tstack) =
-        whd_stack (evars_of clause.evd) (clenv_value clause) in
+        whd_stack ( clause.evd) (clenv_value clause) in
       let nargs = List.length tstack in
       let tstack = match mopt with 
 	| Some m -> 
@@ -1001,7 +1001,7 @@ let specialize mopt (c,lbind) g =
 	errorlabstrm "" (str "Cannot infer an instance for " ++
           pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
 	  str ".");
-      Some (evars_of clause.evd), term
+      Some ( clause.evd), term
   in
   tclTHEN 
     (match evars with Some e -> tclEVARS e | _ -> tclIDTAC)
@@ -3164,5 +3164,5 @@ let unify ?(state=full_transparent_state) x y gl =
     in
     let evd = w_unify false (pf_env gl) Reduction.CONV 
       ~flags x y (Evd.create_evar_defs (project gl))
-    in tclEVARS (Evd.evars_of evd) gl
+    in tclEVARS ( evd) gl
   with _ -> tclFAIL 0 (str"Not unifiable") gl