diff options
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 648d68f27..d1b14e3d9 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1810,9 +1810,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)) |