diff options
| author | Hugo Herbelin | 2018-10-30 11:55:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-30 16:01:32 +0100 |
| commit | 3e71cbf27f18fc494caaea6a20631da5ef9e7d2b (patch) | |
| tree | 20817d69d270be309daa360f61e0322f96e103c9 | |
| parent | 56c3ae6296994cc288d4931110118617bb5bb978 (diff) | |
Adapting to Coq PR #8718: declare_definition now takes a UState.t.
Also use new predefined Lemmas.no_kook.
| -rw-r--r-- | tuto1/src/simple_declare.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml index 2737793d69..4130bab2f4 100644 --- a/tuto1/src/simple_declare.ml +++ b/tuto1/src/simple_declare.ml @@ -9,9 +9,9 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = (Option.List.cons tyopt [body]) in let sigma = Evd.restrict_universe_context sigma uvars in let univs = Evd.check_univ_decl ~poly sigma udecl in - let ubinders = Evd.universe_binders sigma in + let ucontext = Evd.evar_universe_context sigma in let ce = Declare.definition_entry ?types:tyopt ~univs body in - DeclareDef.declare_definition ident k ce ubinders imps hook + DeclareDef.declare_definition ident k ce ucontext imps hook let packed_declare_definition ident value_with_constraints = let body, ctx = value_with_constraints in @@ -19,7 +19,6 @@ let packed_declare_definition ident value_with_constraints = let k = (Decl_kinds.Global, Flags.is_universe_polymorphism(), 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) + ignore (edeclare ident k ~opaque:false sigma udecl body None [] Lemmas.no_hook) (* But this definition cannot be undone by Reset ident *) |