diff options
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 11 |
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 () |