From 4f81cc44e5af01f40ad972a7285edd2c40c178c7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 7 Mar 2020 01:04:46 -0500
Subject: [proof] Start of mutual definition save refactoring.

First commit of a series that will unify (and enforce) the handling of
mutual constants. We will split this in several commits as to easy
debugging / bisect in case of problems.

In this first commit, we move the actual declare logic to a common
place.
---
 vernac/declareDef.mli | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index fb1fc9242c..a62dea05ff 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -59,6 +59,18 @@ val declare_assumption
   -> Entries.parameter_entry
   -> GlobRef.t
 
+val declare_mutually_recursive
+  : opaque:bool
+  -> univs:Entries.universes_entry
+  -> scope:locality
+  -> kind:Decls.logical_kind
+  -> ubind:UnivNames.universe_binders
+  -> Names.variable list
+  -> Constr.constr list
+  -> Constr.types list
+  -> Impargs.manual_implicits list
+  -> Names.GlobRef.t list
+
 val prepare_definition
   :  allow_evars:bool
   -> ?opaque:bool
-- 
cgit v1.2.3


From a0296d51711cdd42f201b9d0e937266984a20944 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 01:49:07 -0400
Subject: [proof] Factorize call info message in mutual declarations

---
 vernac/declareDef.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index a62dea05ff..38a2da4261 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -60,7 +60,9 @@ val declare_assumption
   -> GlobRef.t
 
 val declare_mutually_recursive
-  : opaque:bool
+  : cofix:bool
+  -> indexes:int array option
+  -> opaque:bool
   -> univs:Entries.universes_entry
   -> scope:locality
   -> kind:Decls.logical_kind
-- 
cgit v1.2.3


From 09d6197bd11ed4a323b335118ae749d7caefeb55 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 01:51:37 -0400
Subject: [proof] [mutual] Factorize notation declaration.

---
 vernac/declareDef.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 38a2da4261..971f924c6c 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -67,6 +67,7 @@ val declare_mutually_recursive
   -> scope:locality
   -> kind:Decls.logical_kind
   -> ubind:UnivNames.universe_binders
+  -> ntns:Vernacexpr.decl_notation list
   -> Names.variable list
   -> Constr.constr list
   -> Constr.types list
-- 
cgit v1.2.3


From affb6ac843380e8e134fd89380746f2f6f8c11de Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 02:09:03 -0400
Subject: [proof] [mutual] Factorize mutual body construction.

---
 vernac/declareDef.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 971f924c6c..6400fa8ee7 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -59,6 +59,14 @@ val declare_assumption
   -> Entries.parameter_entry
   -> GlobRef.t
 
+(* Returns [uvars, bodies, indexes], [possible_indexes] determines if
+   we are in a fix / cofix case *)
+val mutual_make_bodies
+  : fixnames:'a list
+  -> rec_declaration:Constr.rec_declaration
+  -> possible_indexes:int list list option
+  -> Univ.LSet.t * Constr.constr list * int array option
+
 val declare_mutually_recursive
   : cofix:bool
   -> indexes:int array option
-- 
cgit v1.2.3


From a15e584571a4e153e98a11c93d12759c45ea2dcd Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 02:22:59 -0400
Subject: [proof] [mutual] Factorize universe handling.

Note that we had to introduce a `restrict_ucontext` parameter to be
faithful to the implementation in obligations, however this looks like
a bug.
---
 vernac/declareDef.mli | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 6400fa8ee7..05a38c039d 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -59,25 +59,18 @@ val declare_assumption
   -> Entries.parameter_entry
   -> GlobRef.t
 
-(* Returns [uvars, bodies, indexes], [possible_indexes] determines if
-   we are in a fix / cofix case *)
-val mutual_make_bodies
-  : fixnames:'a list
-  -> rec_declaration:Constr.rec_declaration
-  -> possible_indexes:int list list option
-  -> Univ.LSet.t * Constr.constr list * int array option
-
 val declare_mutually_recursive
-  : cofix:bool
-  -> indexes:int array option
-  -> opaque:bool
-  -> univs:Entries.universes_entry
+  : opaque:bool
   -> scope:locality
   -> kind:Decls.logical_kind
-  -> ubind:UnivNames.universe_binders
+  -> poly:bool
+  -> uctx:UState.t
+  -> udecl:UState.universe_decl
   -> ntns:Vernacexpr.decl_notation list
+  -> rec_declaration:Constr.rec_declaration
+  -> possible_indexes:int list list option
+  -> restrict_ucontext:bool
   -> Names.variable list
-  -> Constr.constr list
   -> Constr.types list
   -> Impargs.manual_implicits list
   -> Names.GlobRef.t list
-- 
cgit v1.2.3


From 8129fb2abce6ba2e5ddd1f384618bb2fb8f817b5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 02:47:01 -0400
Subject: [proof] [mutual] Factorize mutual per-entry information

We move `Recthm` to `DeclareDef` so it is shared by interactive and
direct fixpoint declaration.

This is the last step before unifying both paths.
---
 vernac/declareDef.mli | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 05a38c039d..995aa0ceff 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -59,6 +59,19 @@ val declare_assumption
   -> Entries.parameter_entry
   -> GlobRef.t
 
+module Recthm : sig
+  type t =
+    { name : Id.t
+    (** Name of theorem *)
+    ; typ : Constr.t
+    (** Type of theorem  *)
+    ; args : Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+end
+
 val declare_mutually_recursive
   : opaque:bool
   -> scope:locality
@@ -70,9 +83,7 @@ val declare_mutually_recursive
   -> rec_declaration:Constr.rec_declaration
   -> possible_indexes:int list list option
   -> restrict_ucontext:bool
-  -> Names.variable list
-  -> Constr.types list
-  -> Impargs.manual_implicits list
+  -> Recthm.t list
   -> Names.GlobRef.t list
 
 val prepare_definition
-- 
cgit v1.2.3


From b623017fea475b7b91c99f462b0fe2458bfe91e7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 24 Mar 2020 23:52:31 -0400
Subject: [declare] make restrict_ucontext an optional parameter.

The current API does just exist as a workaround for a bug.
---
 vernac/declareDef.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 995aa0ceff..1d7fd3a3bf 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -82,7 +82,9 @@ val declare_mutually_recursive
   -> ntns:Vernacexpr.decl_notation list
   -> rec_declaration:Constr.rec_declaration
   -> possible_indexes:int list list option
-  -> restrict_ucontext:bool
+  -> ?restrict_ucontext:bool
+  (** XXX: restrict_ucontext should be always true, this seems like a
+     bug in obligations, so this parameter should go away *)
   -> Recthm.t list
   -> Names.GlobRef.t list
 
-- 
cgit v1.2.3