diff options
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 2 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 0b005a2341..73d94c2a51 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -287,7 +287,7 @@ VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY | ![ proof_query ] [ "ExploreProof" ] -> { fun ~pstate -> let sigma, env = Pfedit.get_current_context pstate in - let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in + let pprf = Proof.partial_proof (Proof_global.get_proof pstate) in Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) } diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 1e582e6456..eb8161c2bb 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -7,7 +7,7 @@ let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = DeclareDef.declare_definition ident k ce ubinders imps ?hook_data let declare_definition ~poly ident sigma body = - let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in + let k = Decl_kinds.(Global ImportDefaultBehavior, poly, Definition) in let udecl = UState.default_univ_decl in edeclare ident k ~opaque:false sigma udecl body None [] |