diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-10-27 12:49:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-10-27 12:51:01 +0100 |
| commit | 7443b875c6de2b674a046c854af8b1f7d32d6b0c (patch) | |
| tree | 847086b4a9b96d5bd05d2ece7c78103017f876de /plugins/setoid_ring/newring.ml4 | |
| parent | 9655b03d8d3f2b256b6ba71eb4b48bd767d4974b (diff) | |
Removing an Evd.merge in Newring.
Diffstat (limited to 'plugins/setoid_ring/newring.ml4')
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 2006a2a61..96ab4f1e1 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -193,9 +193,9 @@ let ltac_record flds = let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c) -let dummy_goal env = +let dummy_goal env sigma = let (gl,_,sigma) = - Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in + Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in {Evd.it = gl; Evd.sigma = sigma} let constr_of v = match Value.to_constr v with @@ -212,12 +212,8 @@ let exec_tactic env evd n f args = let getter = Tacexp(TacFun(List.map(fun id -> Some id) lid, Tacintern.glob_tactic(tacticIn get_res))) in - let gls = - (fun gl -> - let sigma = gl.Evd.sigma in - tclTHEN (Refiner.tclEVARS (Evd.merge sigma evd)) - (Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter])))) gl) - (dummy_goal env) in + let gl = dummy_goal env evd in + let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd |