From 43d381ab20035f64ce2edea8639fcd9e1d0453bc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 14:09:30 +0200 Subject: [declare] Move proof information to declare. At this point the record in lemmas was just a stub; next commit will stop exposing the internals of mutual information, and pave the way for the refactoring of `Info.t` handling in the Declare interface. --- doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/plugin_tutorial/tuto1/src') diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 8c2090f3be..dee407bbe4 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 = Declare.get_current_context pstate in - let pprf = Proof.partial_proof (Declare.Proof.get_proof pstate) in + let pprf = Proof.partial_proof (Declare.Proof.get pstate) in Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) } -- cgit v1.2.3 From 1f121ebf2990dc25899f2f3eb138eddd147483cf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 15 May 2020 02:42:38 +0200 Subject: [declare] Refactor constant information into a record. This improves the interface, and allows even more sealing of the API. This is yet work in progress. --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/plugin_tutorial/tuto1/src') diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index e9e866c5fb..5431a21b53 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -2,5 +2,5 @@ let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in let scope = Declare.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - Declare.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl - ~opaque:false ~poly ~types:None ~body sigma + let info = Declare.CInfo.make ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly () in + Declare.declare_definition ~name ~info ~types:None ~body sigma -- cgit v1.2.3 From a6d663c85d71b3cce007af23419e8030b8c5ac88 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 14:57:44 +0200 Subject: [declare] [api] Removal of duplicated type aliases. --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/plugin_tutorial/tuto1/src') diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 5431a21b53..73292e0120 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,6 +1,6 @@ let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - let scope = Declare.Global Declare.ImportDefaultBehavior in + let scope = Locality.Global Locality.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in let info = Declare.CInfo.make ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly () in Declare.declare_definition ~name ~info ~types:None ~body sigma -- cgit v1.2.3 From 030bb57d4b7e70d45379cab61903b75bf7a41b19 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 16:43:01 +0200 Subject: [declare] Reify Proof.t API into the Proof module. This is in preparation for the next commit which will clean-up the current API flow in `Declare`. --- doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/plugin_tutorial/tuto1/src') diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index dee407bbe4..d24d968c01 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -286,7 +286,7 @@ END VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY | ![ proof_query ] [ "ExploreProof" ] -> { fun ~pstate -> - let sigma, env = Declare.get_current_context pstate in + let sigma, env = Declare.Proof.get_current_context pstate in let pprf = Proof.partial_proof (Declare.Proof.get pstate) in Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) -- cgit v1.2.3 From ea8b9e060dfba9cc8706677e29c26dabaaa87551 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 22 Jun 2020 20:42:39 +0200 Subject: [declare] Improve organization of proof/constant information. We unify information about constants so it is shared among all the paths [interactive, NI, obligations]. IMHO the current setup looks pretty good, with information split into a per-constant record `CInfo.t` and variables affecting mutual definitions at once, which live in `Info.t`. Main information outside our `Info` record is `opaque`, which is provided at different moments in several cases. There are a few nits regarding interactive proofs, which will go away in the next commits. --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'doc/plugin_tutorial/tuto1/src') diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 73292e0120..4d0105ea9d 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -2,5 +2,6 @@ let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in let scope = Locality.Global Locality.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - let info = Declare.CInfo.make ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly () in - Declare.declare_definition ~name ~info ~types:None ~body sigma + let cinfo = Declare.CInfo.make ~name ~typ:None () in + let info = Declare.Info.make ~scope ~kind ~udecl ~poly () in + Declare.declare_definition ~info ~cinfo ~opaque:false ~body sigma -- cgit v1.2.3