diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-15 21:01:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:18:56 +0100 |
| commit | a5feb9687819c5e7ef0db6e7b74d0e236a296674 (patch) | |
| tree | bfd809fd50c8db88f390e3d5cba22360a0c90724 /tactics | |
| parent | d437078a4ca82f7ca6d19be5ee9452359724f9a0 (diff) | |
Separate checking univ_decls and obtaining universe binder names.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/leminv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 62f3866de..4d1b271d6 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -235,9 +235,9 @@ let inversion_scheme env sigma t sort dep_option inv_op = p, Evd.universe_context ~names:[] ~extensible:true sigma 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 invProof, univs = inversion_scheme env sigma t sort dep inv_op in let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) - ~univs:(snd ctx) invProof in + ~univs invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () |