diff options
| author | Emilio Jesus Gallego Arias | 2019-01-31 02:11:31 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | e4487ac3e914c27a222f8a236b9d1a13dd26c725 (patch) | |
| tree | 15a8dc209d5de8cc9b9925e2edf2e8913e11e842 /doc/plugin_tutorial/tuto1/src | |
| parent | 46a8fe0ef1c06ff1b64082ff87b8725dbbd4989b (diff) | |
[plugin tutorial] Adapt to removal of imperative state.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 14 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.ml | 6 |
2 files changed, 11 insertions, 9 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 4df284d2d9..1d0aca1caf 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -145,10 +145,12 @@ END it gives an error message that is basically impossible to understand. *) VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY -| [ "Cmd9" ] -> - { let p = Proof_global.give_me_the_proof () in - let sigma, env = Pfedit.get_current_context () in - let pprf = Proof.partial_proof p in - Feedback.msg_notice - (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) } +| ![ proof ] [ "Cmd9" ] -> + { fun ~pstate -> + Option.iter (fun (pstate : Proof_global.t) -> + let sigma, env = Pfedit.get_current_context pstate in + let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in + Feedback.msg_notice + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) pstate; + pstate } END diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index e370d37fc4..23f8fbe888 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 ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = +let edeclare ?hook ~ontop 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 @@ -13,13 +13,13 @@ let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = let ubinders = Evd.universe_binders sigma in let ce = Declare.definition_entry ?types:tyopt ~univs body in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ident k ce ubinders imps ?hook_data + DeclareDef.declare_definition ~ontop 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 - ignore (edeclare ident k ~opaque:false sigma udecl body None []) + ignore (edeclare ~ontop:None ident k ~opaque:false sigma udecl body None []) (* But this definition cannot be undone by Reset ident *) |