From 34d85e1e899f8a045659ccc53bfd6a1f5104130b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Sep 2017 17:22:24 +0200
Subject: Use Entries.constant_universes_entry more.

This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
---
 tactics/leminv.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1ee873e0ff..1ae3577edb 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,12 +232,15 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
   let invProof = EConstr.Unsafe.to_constr invProof in
   let p = Evarutil.nf_evars_universes sigma invProof in
-    p, Evd.to_universe_context sigma
+    p, sigma
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
-  let invProof, univs = inversion_scheme env sigma t sort dep inv_op in
-  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
-                               ~univs invProof in
+  let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
+  let univs =
+    let poly = Flags.use_polymorphic_flag () in
+    Evd.const_univ_entry ~poly sigma
+  in
+  let entry = definition_entry ~univs invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
-- 
cgit v1.2.3