From cd29948855c2cbd3f4065170e41f8dbe625e1921 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 9 Sep 2017 14:00:42 +0200 Subject: Don't lose names in UState.universe_context. We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it. --- plugins/setoid_ring/newring.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/setoid_ring/newring.ml') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index d0fe1f957..b8fae2494 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = 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 - Array.map nf !tactic_res, snd (Evd.universe_context evd) + Array.map nf !tactic_res, snd (Evd.universe_context ~names:[] ~extensible:true evd) let stdlib_modules = [["Coq";"Setoids";"Setoid"]; -- cgit v1.2.3