Removing uselessly duplicated function in Evd.

7 files changed, 6 insertions, 12 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 1af8565bdb..ae382cab45 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -766,10 +766,6 @@ let cmap f evd =
 (* spiwack: deprecated *)
 let create_evar_defs sigma = { sigma with
   conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty }
-(* spiwack: tentatively deprecated *)
-let create_goal_evar_defs sigma = { sigma with
-   (* conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } *)
-  metas=Metamap.empty } 
 
 let empty = {
   defn_evars = EvMap.empty;
diff --git a/engine/evd.mli b/engine/evd.mli
index e240ebc310..0902191818 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -611,8 +611,6 @@ val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
 val create_evar_defs      : evar_map -> evar_map
 (** Create an [evar_map] with empty meta map: *)
 
-val create_goal_evar_defs : evar_map -> evar_map
-
 (** {5 Summary names} *)
 
 val evar_counter_summary_name : string
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 714cd86341..f8ddd5f80c 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -86,7 +86,7 @@ Please \"suppose\" something or \"end\" it now."
       | _ -> ()
 
 let mk_evd metalist gls =
-  let evd0= create_goal_evar_defs (sig_sig gls) in
+  let evd0= clear_metas (sig_sig gls) in
   let add_one (meta,typ) evd =
     meta_declare meta typ evd in
     List.fold_right add_one metalist evd0
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index a2cccc0e0b..16146f4846 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -119,7 +119,7 @@ let clenv_environments evd bound t =
   clrec (evd,[]) bound t
 
 let mk_clenv_from_env env sigma n (c,cty) =
-  let evd = create_goal_evar_defs sigma in
+  let evd = clear_metas sigma in
   let (evd,args,concl) = clenv_environments evd n cty in
   { templval = mk_freelisted (applist (c,args));
     templtyp = mk_freelisted concl;
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index aaa49f1169..f54d4c4470 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -121,7 +121,7 @@ let unify ?(flags=fail_quick_unif_flags) m =
   Proofview.Goal.enter begin fun gl ->
     let env = Tacmach.New.pf_env gl in
     let n = Tacmach.New.pf_nf_concl gl in
-    let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in
+    let evd = clear_metas (Proofview.Goal.sigma gl) in
     try
       let evd' = w_unify env evd CONV ~flags m n in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5c48995fc7..7d101b4c72 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -95,12 +95,12 @@ let check_typability env sigma c =
    forces the user to give them in order). *)
 
 let clear_hyps env sigma ids sign cl =
-  let evdref = ref (Evd.create_goal_evar_defs sigma) in
+  let evdref = ref (Evd.clear_metas sigma) in
   let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in
   (hyps, cl, !evdref)
 
 let clear_hyps2 env sigma ids sign t cl =
-  let evdref = ref (Evd.create_goal_evar_defs sigma) in
+  let evdref = ref (Evd.clear_metas sigma) in
   let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
   (hyps, t, cl, !evdref)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ec0e1d2f4e..a10d8a0747 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1095,7 +1095,7 @@ let minimal_free_rels_rec env sigma =
 
 let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let sigdata = find_sigma_data env sort_of_ty in
-  let evdref = ref (Evd.create_goal_evar_defs sigma) in
+  let evdref = ref (Evd.clear_metas sigma) in
   let rec sigrec_clausal_form siglen p_i =
     if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)