diff options
| author | Pierre-Marie Pédrot | 2018-04-30 09:57:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-04-30 09:57:24 +0200 |
| commit | df9fe1be977c2c856b11a842233598f8a791db49 (patch) | |
| tree | a7f25d877acda30f02627f710002c682f61a39e1 /plugins/setoid_ring | |
| parent | c1e12fbc64c39739e4a9f7bbf92e42f1bcb6be24 (diff) | |
| parent | dbc820f0df53218e730eba34b44a3b1901f13b9e (diff) | |
Merge PR #6935: Separate universe minimization and evar normalization functions
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 99bb8440c6..33c30e4d38 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -186,8 +186,8 @@ let dummy_goal env sigma = Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in {Evd.it = gl; Evd.sigma = sigma} -let constr_of v = match Value.to_constr v with - | Some c -> EConstr.Unsafe.to_constr c +let constr_of evd v = match Value.to_constr v with + | Some c -> EConstr.to_constr evd c | None -> failwith "Ring.exec_tactic: anomaly" let tactic_res = ref [||] @@ -221,8 +221,8 @@ let exec_tactic env evd n f args = (** Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in - let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - let nf c = nf (constr_of c) in + let evd = Evd.minimize_universes (Refiner.project gls) in + let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd let stdlib_modules = |