aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-15 21:01:57 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-24 19:18:56 +0100
commita5feb9687819c5e7ef0db6e7b74d0e236a296674 (patch)
treebfd809fd50c8db88f390e3d5cba22360a0c90724 /tactics
parentd437078a4ca82f7ca6d19be5ee9452359724f9a0 (diff)
Separate checking univ_decls and obtaining universe binder names.
Diffstat (limited to 'tactics')
-rw-r--r--tactics/leminv.ml4
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
()