From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Oct 2015 12:36:20 -0400
Subject: Univs: local names handling.

Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
---
 plugins/setoid_ring/newring.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/setoid_ring')

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"];
-- 
cgit v1.2.3