aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 1c4ba88237..c7185ff25e 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -220,7 +220,7 @@ let exec_tactic env evd n f args =
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
+ Array.map (fun x -> nf (constr_of x)) !res, snd (Evd.universe_context evd)
let stdlib_modules =
[["Coq";"Setoids";"Setoid"];