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.
---
 tactics/leminv.ml  | 3 ++-
 tactics/rewrite.ml | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 42d22bc3c4..8ca622171f 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -229,7 +229,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
-  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:ctx invProof in
+  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
+			       ~univs:(snd ctx) invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 0811708695..e8a7c0f600 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1806,9 +1806,9 @@ let declare_projection n instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
+  let pl, ctx = Evd.universe_context sigma in
   let cst = 
-    Declare.definition_entry ~types:typ ~poly
-      ~univs:(Evd.universe_context sigma) term
+    Declare.definition_entry ~types:typ ~poly ~univs:ctx term
   in
     ignore(Declare.declare_constant n 
 	   (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
-- 
cgit v1.2.3