diff options
| author | Pierre-Marie Pédrot | 2015-09-27 14:16:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-27 14:17:56 +0200 |
| commit | ca14b0bb67c9db000736333a056fc147c6f5199c (patch) | |
| tree | 45892d06e0f92adb2d08786cfa04cb64350806a8 /proofs | |
| parent | f52826877059858fb3fcd4314c629ed63d90a042 (diff) | |
Removing uselessly duplicated function in Evd.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 4 |
3 files changed, 4 insertions, 4 deletions
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) |