diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/leminv.ml | 3 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 4 |
2 files changed, 4 insertions, 3 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 42d22bc3c4..8ca622171f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -229,7 +229,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = 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 entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:ctx invProof in + let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) + ~univs:(snd ctx) invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 0811708695..e8a7c0f600 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1806,9 +1806,9 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in + let pl, ctx = Evd.universe_context sigma in let cst = - Declare.definition_entry ~types:typ ~poly - ~univs:(Evd.universe_context sigma) term + Declare.definition_entry ~types:typ ~poly ~univs:ctx term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) |