From 56ffe818ab7706a82d79b538fdf3af8b23d95f40 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 03:07:42 -0400
Subject: [declare] [obligations] Refactor preparation of obligation entry

Preparation of obligation/program entries requires low-level
manipulation that does break the abstraction over `proof_entry`; we
thus introduce `prepare_obligation`, and move the code that prepares
the obligation entry to its own module.

This seems to improve separation of concerns, and helps clarify the
two of three current models in which Coq operates w.r.t. definitions:

- single, ground entries with possibly mutual definitions [regular lemmas]
- single, non-ground entries with possibly mutual definitions [obligations]
- multiple entries [equations]
---
 doc/plugin_tutorial/tuto1/src/simple_declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/plugin_tutorial')

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 2fdca15552..3b906324f4 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,5 +1,5 @@
 let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
-  let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
+  let sigma, ce = DeclareDef.prepare_definition
       ~opaque ~poly sigma ~udecl ~types:tyopt ~body in
   let uctx = Evd.evar_universe_context sigma in
   let ubind = Evd.universe_binders sigma in
-- 
cgit v1.2.3


From 8fbc927ac40cc707b1a940d8339a2a289755d533 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 16:34:30 -0400
Subject: [declareDef] More consistent handling of universe binders

The only reasons that `prepare_definition` returned a sigma were:
- to obtain the universe binders to be passed to declare
- to obtain the UState.t to be passed to the equations hook

We handle this automatically now; it seems like a reasonably good API
improvement.

However, it is not clear what we do now is right for all cases; must
check.
---
 doc/plugin_tutorial/tuto1/src/simple_declare.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'doc/plugin_tutorial')

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 3b906324f4..a2783d80e8 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,10 +1,7 @@
 let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
-  let sigma, ce = DeclareDef.prepare_definition
+  let ce = DeclareDef.prepare_definition
       ~opaque ~poly sigma ~udecl ~types:tyopt ~body in
-  let uctx = Evd.evar_universe_context sigma in
-  let ubind = Evd.universe_binders sigma in
-  let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ~name ~scope ~kind ~ubind ce ~impargs ?hook_data
+  DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ce
 
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
-- 
cgit v1.2.3


From 7d46a32dc928af64e3e111d6d62caa00f93c427c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 18 Mar 2020 05:35:41 -0400
Subject: [declare] Fuse prepare and declare for the non-interactive path.

This will allow to share the definition metadata for example with
obligations; a bit more work is needed to finally move the preparation
of interactive proofs from Proof_global to `prepare_entry`.
---
 doc/plugin_tutorial/tuto1/src/simple_declare.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'doc/plugin_tutorial')

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index a2783d80e8..8c4dc0e8a6 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,7 +1,6 @@
 let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
-  let ce = DeclareDef.prepare_definition
-      ~opaque ~poly sigma ~udecl ~types:tyopt ~body in
-  DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ce
+  DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook
+    ~opaque ~poly ~udecl ~types:tyopt ~body sigma
 
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
-- 
cgit v1.2.3