Removing almost all new_untyped_evar, and a bunch of Evd.add.

Ultimately all evars should be created with respect to a given
evar map, instead of using a global counter.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16783 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 26 insertions, 30 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index b13d2ea29..10b3febb3 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -47,14 +47,14 @@ let rec subst_evar evar def n c =
     | _ -> map_constr_with_binders (fun n->n+1) (subst_evar evar def) n c
 
 let subst_evar_in_evm evar def evm =
-  Evd.fold
-    (fun ev evi acc ->
-       let evar_body = match evi.evar_body with
-	 | Evd.Evar_empty -> Evd.Evar_empty
-	 | Evd.Evar_defined c -> Evd.Evar_defined (subst_evar evar def 0 c) in
-       let evar_concl = subst_evar evar def 0 evi.evar_concl in
-       Evd.add acc ev {evi with evar_body=evar_body; evar_concl=evar_concl}
-    ) evm empty
+  let map ev evi =
+    let evar_body = match evi.evar_body with
+      | Evd.Evar_empty -> Evd.Evar_empty
+      | Evd.Evar_defined c -> Evd.Evar_defined (subst_evar evar def 0 c) in
+    let evar_concl = subst_evar evar def 0 evi.evar_concl in
+    {evi with evar_body=evar_body; evar_concl=evar_concl}
+  in
+  Evd.raw_map map evm
 
 (* Tries to define ev by c in evd. Fails if ev := c1 and c1 /= c ev :
  * T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated
@@ -80,21 +80,16 @@ let rec safe_define evm ev c =
 	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 () =
-    let ev = Evarutil.new_untyped_evar() in
-    if Evd.is_evar evm ev then really_new_evar() else ev in
-  let add_gen_evar (cl,gen,evm) ev ty : signature =
-    let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val ty) in
-    (cl,ev::gen,evm) in
+  let env = Environ.empty_named_context_val in
+  let fold_new_evar evm _ = Evarutil.new_pure_evar evm env mkProp in
   let rec mksubst b = function
     | [] -> []
     | a::tl -> b::(mksubst (a::b) tl) in
-  let evl = List.map (fun _ -> really_new_evar()) ctx in
+  let (evm, evl) = List.fold_map fold_new_evar evm ctx in
   let evcl = List.map (fun i -> mkEvar (i,[||])) evl in
-  let substl = List.rev (mksubst [] (evcl)) in
-  let ctx = List.map2 (fun s t -> substnl s 0 t) substl ctx in
-  let sign = List.fold_left2 add_gen_evar (cl,gen,evm) (List.rev evl) ctx in
-  sign,evcl
+(*   let substl = List.rev (mksubst [] (evcl)) in *)
+(*   let ctx = List.map2 (fun s t -> substnl s 0 t) substl ctx in *)
+  (cl, evl @ gen, evm), evcl
 
 (* TODO : for full proof-irrelevance in the search, provide a real
    compare function for constr instead of Pervasive's one! *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9f24fc158..118a13ead 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -889,11 +889,6 @@ let out_def = function
   | Some def -> def
   | None -> error "Program Fixpoint needs defined bodies."
 
-let collect_evars_of_term evd c ty =
-  let evars = Int.Set.union (evars_of_term c) (evars_of_term ty) in
-    Int.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
-      evars Evd.empty
-      
 let do_program_recursive local fixkind fixl ntns =
   let isfix = fixkind != Obligations.IsCoFixpoint in
   let (env, rec_sign, evd), fix, info = 
@@ -911,9 +906,8 @@ let do_program_recursive local fixkind fixl ntns =
     and typ =
       nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
     in
-    let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ = 
-      Obligations.eterm_obligations env id evm
+      Obligations.eterm_obligations env id evd
 	(List.length rec_sign) def typ
     in (id, def, typ, imps, evars)
   in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 3d85d3faf..0f49662c8 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -202,12 +202,17 @@ let sort_dependencies evl =
 
 open Environ
 
+let collect_evars_of_term c ty =
+  Int.Set.union (Evarutil.evars_of_term c) (Evarutil.evars_of_term ty)
+
 let eterm_obligations env name evm fs ?status t ty = 
   (* 'Serialize' the evars *)
+  let evars = collect_evars_of_term t ty in
   let nc = Environ.named_context env in
   let nc_len = Context.named_context_length nc in
   let evm = Evarutil.nf_evar_map_undefined evm in
   let evl = Evarutil.non_instantiated evm in
+  let evl = ExistentialMap.filter (fun ev _ -> Int.Set.mem ev evars) evl in
   let evl = ExistentialMap.bindings evl in
   let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
   let sevl = sort_dependencies evl in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 5c59987aa..e0dc6c3a3 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -221,11 +221,13 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 let structure_signature ctx =
   let rec deps_to_evar evm l =
     match l with [] -> Evd.empty
-      | [(_,_,typ)] -> Evd.add evm (Evarutil.new_untyped_evar())
-	  (Evd.make_evar Environ.empty_named_context_val typ)
+      | [(_,_,typ)] ->
+        let env = Environ.empty_named_context_val in
+        let (evm, _) = Evarutil.new_pure_evar evm env typ in
+        evm
       | (_,_,typ)::tl ->
-	  let ev = Evarutil.new_untyped_evar() in
-	  let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val typ) in
+          let env = Environ.empty_named_context_val in
+          let (evm, ev) = Evarutil.new_pure_evar evm env typ in
 	  let new_tl = Util.List.map_i
 	    (fun pos (n,c,t) -> n,c,
 	       Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in