diff options
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_check.ml | 2 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.ml | 9 |
2 files changed, 6 insertions, 5 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml index 1f636c531a..2949adde73 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_check.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml @@ -6,7 +6,7 @@ let simple_check1 value_with_constraints = (* The point of renaming is to make sure the bound names printed by Check can be re-used in `apply with` tactics that use bound names to refer to arguments. *) - let j = Termops.on_judgment EConstr.of_constr + let j = Environ.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing (Global.env()) (EConstr.to_constr evd evalue)) in let {Environ.uj_type=x}=j in x diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 9d10a8ba72..e370d37fc4 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,5 +1,5 @@ (* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *) -let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = +let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = let sigma = Evd.minimize_universes sigma in let body = EConstr.to_constr sigma body in let tyopt = Option.map (EConstr.to_constr sigma) tyopt in @@ -9,16 +9,17 @@ 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 uctx = Evd.evar_universe_context sigma in let ubinders = Evd.universe_binders sigma in let ce = Declare.definition_entry ?types:tyopt ~univs body in - DeclareDef.declare_definition ident k ce ubinders imps ~hook + let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + DeclareDef.declare_definition ident k ce ubinders imps ?hook_data 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, 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) + ignore (edeclare ident k ~opaque:false sigma udecl body None []) (* But this definition cannot be undone by Reset ident *) |