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.

1 files changed, 7 insertions, 4 deletions

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1ee873e0f..1ae3577ed 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
   ()