diff options
Diffstat (limited to 'tuto1/src/simple_declare.ml')
| -rw-r--r-- | tuto1/src/simple_declare.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml index 2737793d69..af4dd5bddf 100644 --- a/tuto1/src/simple_declare.ml +++ b/tuto1/src/simple_declare.ml @@ -13,11 +13,10 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = let ce = Declare.definition_entry ?types:tyopt ~univs body in DeclareDef.declare_definition ident k ce ubinders imps hook -let packed_declare_definition ident value_with_constraints = +let packed_declare_definition ~poly ident value_with_constraints = let body, ctx = value_with_constraints in let sigma = Evd.from_ctx ctx in - let k = (Decl_kinds.Global, - Flags.is_universe_polymorphism(), Decl_kinds.Definition) in + let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in let udecl = UState.default_univ_decl in let nohook = Lemmas.mk_hook (fun _ x -> ()) in ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook) |