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.
---
 tactics/proof_global.ml  |  8 --------
 tactics/proof_global.mli |  4 +---
 vernac/comFixpoint.ml    |  6 ++----
 vernac/declareDef.ml     |  7 +++++++
 vernac/declareDef.mli    | 12 ++++++++++++
 vernac/declareObl.ml     |  6 ++----
 6 files changed, 24 insertions(+), 19 deletions(-)

diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 7fd1634dcf..623e6b8a42 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -8,14 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(***********************************************************************)
-(*                                                                     *)
-(*      This module defines proof facilities relevant to the           *)
-(*      toplevel. In particular it defines the global proof            *)
-(*      environment.                                                   *)
-(*                                                                     *)
-(***********************************************************************)
-
 open Util
 open Names
 open Context
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index f1281d1291..e1c75c0649 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -8,9 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** This module defines proof facilities relevant to the
-     toplevel. In particular it defines the global proof
-     environment. *)
+(** State for interactive proofs. *)
 
 type t
 
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0a70954dd2..4e5b1d7205 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -279,12 +279,10 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let fiximps = List.map (fun (n,r,p) -> r) fiximps in
   let evd = Evd.from_ctx ctx in
   let evd = Evd.restrict_universe_context evd vars in
-  let ctx = Evd.check_univ_decl ~poly evd pl in
+  let univs = Evd.check_univ_decl ~poly evd pl in
   let ubind = Evd.universe_binders evd in
   let _ : GlobRef.t list =
-    List.map4 (fun name body types impargs ->
-        let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in
-        DeclareDef.declare_definition ~name ~scope ~kind:fix_kind ~ubind ~impargs ce)
+    DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind
       fixnames fixdecls fixtypes fiximps
   in
   Declare.recursive_message (not cofix) gidx fixnames;
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 09582f4ef2..edf7ed9dc3 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,6 +69,13 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   end;
   dref
 
+let declare_mutually_recursive ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps =
+  CList.map4
+    (fun name body types impargs ->
+       let ce = Declare.definition_entry ~opaque ~types ~univs body in
+       declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
+    fixnames fixdecls fixtypes fiximps
+
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
     Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
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
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index c13e884736..bd3f6e2891 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -467,10 +467,7 @@ let declare_mutual_definition l =
   let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
   let ubind = UnivNames.empty_binders in
   let kns =
-    List.map4
-      (fun name body types impargs ->
-         let ce = Declare.definition_entry ~opaque ~types ~univs body in
-         DeclareDef.declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
+    DeclareDef.declare_mutually_recursive ~scope ~opaque ~univs ~kind ~ubind
       fixnames fixdecls fixtypes fiximps
   in
   (* Declare notations *)
@@ -478,6 +475,7 @@ let declare_mutual_definition l =
     (Metasyntax.add_notation_interpretation (Global.env ()))
     first.prg_notations;
   Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
+  (* Only for the first constant *)
   let dref = List.hd kns in
   DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref });
   List.iter progmap_remove l;
-- 
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/comFixpoint.ml |  5 ++---
 vernac/declareDef.ml  | 15 +++++++++------
 vernac/declareDef.mli |  4 +++-
 vernac/declareObl.ml  |  4 ++--
 4 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 4e5b1d7205..55ef0f67d6 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -264,7 +264,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   (* We shortcut the proof process *)
   let fixdefs = List.map Option.get fixdefs in
   let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let vars, fixdecls, gidx =
+  let vars, fixdecls, indexes =
     if not cofix then
       let env = Global.env() in
       let indexes = Pretyping.search_guard env indexes fixdecls in
@@ -282,10 +282,9 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let univs = Evd.check_univ_decl ~poly evd pl in
   let ubind = Evd.universe_binders evd in
   let _ : GlobRef.t list =
-    DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind
+    DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind
       fixnames fixdecls fixtypes fiximps
   in
-  Declare.recursive_message (not cofix) gidx fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   ()
 
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index edf7ed9dc3..9708f43e53 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,12 +69,15 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   end;
   dref
 
-let declare_mutually_recursive ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps =
-  CList.map4
-    (fun name body types impargs ->
-       let ce = Declare.definition_entry ~opaque ~types ~univs body in
-       declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
-    fixnames fixdecls fixtypes fiximps
+let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps =
+  let csts = CList.map4
+      (fun name body types impargs ->
+         let ce = Declare.definition_entry ~opaque ~types ~univs body in
+         declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
+      fixnames fixdecls fixtypes fiximps
+  in
+  Declare.recursive_message (not cofix) indexes fixnames;
+  csts
 
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
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
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index bd3f6e2891..b2d77f4f38 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -466,15 +466,15 @@ let declare_mutual_definition l =
   let fix_exn = Hook.get get_fix_exn () in
   let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
   let ubind = UnivNames.empty_binders in
+  let cofix = fixkind = IsCoFixpoint in
   let kns =
-    DeclareDef.declare_mutually_recursive ~scope ~opaque ~univs ~kind ~ubind
+    DeclareDef.declare_mutually_recursive ~cofix ~indexes ~scope ~opaque ~univs ~kind ~ubind
       fixnames fixdecls fixtypes fiximps
   in
   (* Declare notations *)
   List.iter
     (Metasyntax.add_notation_interpretation (Global.env ()))
     first.prg_notations;
-  Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
   (* Only for the first constant *)
   let dref = List.hd kns in
   DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref });
-- 
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/comFixpoint.ml | 3 +--
 vernac/declareDef.ml  | 3 ++-
 vernac/declareDef.mli | 1 +
 vernac/declareObl.ml  | 7 ++-----
 4 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 55ef0f67d6..ced9656218 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -282,10 +282,9 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let univs = Evd.check_univ_decl ~poly evd pl in
   let ubind = Evd.universe_binders evd in
   let _ : GlobRef.t list =
-    DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind
+    DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind ~ntns
       fixnames fixdecls fixtypes fiximps
   in
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   ()
 
 let extract_decreasing_argument ~structonly { CAst.v = v; _ } =
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 9708f43e53..b3bcf58b4a 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,7 +69,7 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   end;
   dref
 
-let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps =
+let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps =
   let csts = CList.map4
       (fun name body types impargs ->
          let ce = Declare.definition_entry ~opaque ~types ~univs body in
@@ -77,6 +77,7 @@ let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubin
       fixnames fixdecls fixtypes fiximps
   in
   Declare.recursive_message (not cofix) indexes fixnames;
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   csts
 
 let warn_let_as_axiom =
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
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index b2d77f4f38..e530a6e494 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -467,14 +467,11 @@ let declare_mutual_definition l =
   let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
   let ubind = UnivNames.empty_binders in
   let cofix = fixkind = IsCoFixpoint in
+  let ntns = first.prg_notations in
   let kns =
-    DeclareDef.declare_mutually_recursive ~cofix ~indexes ~scope ~opaque ~univs ~kind ~ubind
+    DeclareDef.declare_mutually_recursive ~cofix ~indexes ~scope ~opaque ~univs ~kind ~ubind ~ntns
       fixnames fixdecls fixtypes fiximps
   in
-  (* Declare notations *)
-  List.iter
-    (Metasyntax.add_notation_interpretation (Global.env ()))
-    first.prg_notations;
   (* Only for the first constant *)
   let dref = List.hd kns in
   DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref });
-- 
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/comFixpoint.ml | 21 +++++----------------
 vernac/declareDef.ml  | 13 +++++++++++++
 vernac/declareDef.mli |  8 ++++++++
 vernac/declareObl.ml  | 33 +++++++++++----------------------
 4 files changed, 37 insertions(+), 38 deletions(-)

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index ced9656218..6e6be4fe3a 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -256,26 +256,15 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   lemma
 
 let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
-  let indexes, cofix, fix_kind =
+  let possible_indexes, cofix, fix_kind =
     match indexes with
-    | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint)
-    | None -> [], true, Decls.(IsDefinition CoFixpoint)
+    | Some indexes -> Some indexes, false, Decls.(IsDefinition Fixpoint)
+    | None -> None, true, Decls.(IsDefinition CoFixpoint)
   in
   (* We shortcut the proof process *)
   let fixdefs = List.map Option.get fixdefs in
-  let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let vars, fixdecls, indexes =
-    if not cofix then
-      let env = Global.env() in
-      let indexes = Pretyping.search_guard env indexes fixdecls in
-      let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),fixdecls)) in
-      let fixdecls = List.map_i (fun i _ -> Constr.mkFix ((indexes,i),fixdecls)) 0 fixnames in
-      vars, fixdecls, Some indexes
-    else (* cofix *)
-      let fixdecls = List.map_i (fun i _ -> Constr.mkCoFix (i,fixdecls)) 0 fixnames in
-      let vars = Vars.universes_of_constr (List.hd fixdecls) in
-      vars, fixdecls, None
-  in
+  let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
+  let vars, fixdecls, indexes = DeclareDef.mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in
   let fiximps = List.map (fun (n,r,p) -> r) fiximps in
   let evd = Evd.from_ctx ctx in
   let evd = Evd.restrict_universe_context evd vars in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index b3bcf58b4a..ba84734360 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,6 +69,19 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   end;
   dref
 
+let mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes =
+  match possible_indexes with
+  | Some possible_indexes ->
+    let env = Global.env() in
+    let indexes = Pretyping.search_guard env possible_indexes rec_declaration in
+    let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixnames in
+    vars, fixdecls, Some indexes
+  | None ->
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixnames in
+    let vars = Vars.universes_of_constr (List.hd fixdecls) in
+    vars, fixdecls, None
+
 let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps =
   let csts = CList.map4
       (fun name body types impargs ->
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
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index e530a6e494..73566f47f4 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -441,38 +441,27 @@ let declare_mutual_definition l =
   let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in
   let rvec = Array.of_list fixrs in
   let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in
-  let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in
-  let fixnames = first.prg_deps in
-  let opaque = first.prg_opaque in
-  let indexes, fixdecls =
+  let rec_declaration = (Array.map2 make_annot namevec rvec, arrrec, recvec) in
+  let possible_indexes =
     match fixkind with
     | IsFixpoint wfl ->
-      let possible_indexes =
-        List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes
-      in
-      let indexes =
-        Pretyping.search_guard (Global.env ()) possible_indexes fixdecls
-      in
-      ( Some indexes
-      , List.map_i (fun i _ -> mkFix ((indexes, i), fixdecls)) 0 l
-      )
-    | IsCoFixpoint ->
-      (None, List.map_i (fun i _ -> mkCoFix (i, fixdecls)) 0 l)
+      Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes)
+    | IsCoFixpoint -> None
   in
-  (* Declare the recursive definitions *)
-  let poly = first.prg_poly in
-  let scope = first.prg_scope in
+  (* In the future we will pack all this in a proper record *)
+  let poly, scope, ntns, opaque, fixnames = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque, first.prg_deps in
+  let kind, cofix = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint, false) else Decls.(IsDefinition CoFixpoint, true) in
   let univs = UState.univ_entry ~poly first.prg_ctx in
-  let fix_exn = Hook.get get_fix_exn () in
-  let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
   let ubind = UnivNames.empty_binders in
-  let cofix = fixkind = IsCoFixpoint in
-  let ntns = first.prg_notations in
+  (* XXX: Note that obligations doesn't call restrict_universe_context *)
+  let _vars, fixdecls, indexes = DeclareDef.mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in
+  (* Declare the recursive definitions *)
   let kns =
     DeclareDef.declare_mutually_recursive ~cofix ~indexes ~scope ~opaque ~univs ~kind ~ubind ~ntns
       fixnames fixdecls fixtypes fiximps
   in
   (* Only for the first constant *)
+  let fix_exn = Hook.get get_fix_exn () in
   let dref = List.hd kns in
   DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref });
   List.iter progmap_remove l;
-- 
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/comFixpoint.ml | 18 +++++++-----------
 vernac/declareDef.ml  | 19 +++++++++++++++++--
 vernac/declareDef.mli | 21 +++++++--------------
 vernac/declareObl.ml  | 12 +++++-------
 4 files changed, 36 insertions(+), 34 deletions(-)

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 6e6be4fe3a..0e2d8c1453 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,24 +255,20 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
 
-let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
-  let possible_indexes, cofix, fix_kind =
+let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
+  let possible_indexes, fix_kind =
     match indexes with
-    | Some indexes -> Some indexes, false, Decls.(IsDefinition Fixpoint)
-    | None -> None, true, Decls.(IsDefinition CoFixpoint)
+    | Some indexes -> Some indexes, Decls.(IsDefinition Fixpoint)
+    | None -> None, Decls.(IsDefinition CoFixpoint)
   in
   (* We shortcut the proof process *)
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let vars, fixdecls, indexes = DeclareDef.mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in
   let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-  let evd = Evd.from_ctx ctx in
-  let evd = Evd.restrict_universe_context evd vars in
-  let univs = Evd.check_univ_decl ~poly evd pl in
-  let ubind = Evd.universe_binders evd in
   let _ : GlobRef.t list =
-    DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind ~ntns
-      fixnames fixdecls fixtypes fiximps
+    DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
+      ~possible_indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
+      fixnames fixtypes fiximps
   in
   ()
 
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index ba84734360..de7223ae62 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -82,14 +82,29 @@ let mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes =
     let vars = Vars.universes_of_constr (List.hd fixdecls) in
     vars, fixdecls, None
 
-let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps =
+let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixnames fixtypes fiximps =
+  let vars, fixdecls, indexes =
+    mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in
+  let ubind, univs =
+    (* XXX: Note that obligations don't do this, is that a bug? *)
+    if restrict_ucontext
+    then
+      let evd = Evd.from_ctx uctx in
+      let evd = Evd.restrict_universe_context evd vars in
+      let univs = Evd.check_univ_decl ~poly evd udecl in
+      Evd.universe_binders evd, univs
+    else
+      let univs = UState.univ_entry ~poly uctx in
+      UnivNames.empty_binders, univs
+  in
   let csts = CList.map4
       (fun name body types impargs ->
          let ce = Declare.definition_entry ~opaque ~types ~univs body in
          declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
       fixnames fixdecls fixtypes fiximps
   in
-  Declare.recursive_message (not cofix) indexes fixnames;
+  let isfix = Option.is_empty possible_indexes in
+  Declare.recursive_message isfix indexes fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   csts
 
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
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 73566f47f4..95e9a10d03 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -450,15 +450,13 @@ let declare_mutual_definition l =
   in
   (* In the future we will pack all this in a proper record *)
   let poly, scope, ntns, opaque, fixnames = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque, first.prg_deps in
-  let kind, cofix = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint, false) else Decls.(IsDefinition CoFixpoint, true) in
-  let univs = UState.univ_entry ~poly first.prg_ctx in
-  let ubind = UnivNames.empty_binders in
-  (* XXX: Note that obligations doesn't call restrict_universe_context *)
-  let _vars, fixdecls, indexes = DeclareDef.mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in
+  let kind = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) else Decls.(IsDefinition CoFixpoint) in
   (* Declare the recursive definitions *)
+  let udecl = UState.default_univ_decl in
   let kns =
-    DeclareDef.declare_mutually_recursive ~cofix ~indexes ~scope ~opaque ~univs ~kind ~ubind ~ntns
-      fixnames fixdecls fixtypes fiximps
+    DeclareDef.declare_mutually_recursive ~scope ~opaque ~kind
+      ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes
+      ~poly ~restrict_ucontext:false fixnames fixtypes fiximps
   in
   (* Only for the first constant *)
   let fix_exn = Hook.get get_fix_exn () in
-- 
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/comFixpoint.ml   | 30 ++++++++++++++++--------------
 vernac/declareDef.ml    | 32 +++++++++++++++++++++++---------
 vernac/declareDef.mli   | 17 ++++++++++++++---
 vernac/declareObl.ml    | 13 +++++++++----
 vernac/lemmas.ml        | 21 ++++++---------------
 vernac/lemmas.mli       | 15 +--------------
 vernac/vernacentries.ml |  2 +-
 7 files changed, 70 insertions(+), 60 deletions(-)

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0e2d8c1453..6580495295 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -236,16 +236,22 @@ let interp_fixpoint ~cofix l =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
-  let fix_kind, cofix, indexes = match indexes with
-    | Some indexes -> Decls.Fixpoint, false, indexes
-    | None -> Decls.CoFixpoint, true, []
+let build_recthms ~indexes fixnames fixtypes fiximps =
+  let fix_kind, cofix = match indexes with
+    | Some indexes -> Decls.Fixpoint, false
+    | None -> Decls.CoFixpoint, true
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
-        { Lemmas.Recthm.name; typ
+        { DeclareDef.Recthm.name; typ
         ; args = List.map Context.Rel.Declaration.get_name ctx; impargs})
-      fixnames fixtypes fiximps in
+      fixnames fixtypes fiximps
+  in
+  fix_kind, cofix, thms
+
+let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
+  let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in
+  let indexes = Option.default [] indexes in
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
   let lemma =
@@ -256,19 +262,15 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   lemma
 
 let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
-  let possible_indexes, fix_kind =
-    match indexes with
-    | Some indexes -> Some indexes, Decls.(IsDefinition Fixpoint)
-    | None -> None, Decls.(IsDefinition CoFixpoint)
-  in
   (* We shortcut the proof process *)
+  let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let fiximps = List.map (fun (n,r,p) -> r) fiximps in
+  let fix_kind = Decls.IsDefinition fix_kind in
   let _ : GlobRef.t list =
     DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
-      ~possible_indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
-      fixnames fixtypes fiximps
+      ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
+      fixitems
   in
   ()
 
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index de7223ae62..6e19cf97b0 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,22 +69,35 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   end;
   dref
 
-let mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes =
+let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
   match possible_indexes with
   | Some possible_indexes ->
     let env = Global.env() in
     let indexes = Pretyping.search_guard env possible_indexes rec_declaration in
     let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in
-    let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixnames in
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in
     vars, fixdecls, Some indexes
   | None ->
-    let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixnames in
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in
     let vars = Vars.universes_of_constr (List.hd fixdecls) in
     vars, fixdecls, None
 
-let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixnames fixtypes fiximps =
+module Recthm = struct
+  type t =
+    { name : Names.Id.t
+    (** Name of theorem *)
+    ; typ : Constr.t
+    (** Type of theorem  *)
+    ; args : Names.Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+end
+
+let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixitems =
   let vars, fixdecls, indexes =
-    mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in
+    mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
   let ubind, univs =
     (* XXX: Note that obligations don't do this, is that a bug? *)
     if restrict_ucontext
@@ -97,13 +110,14 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re
       let univs = UState.univ_entry ~poly uctx in
       UnivNames.empty_binders, univs
   in
-  let csts = CList.map4
-      (fun name body types impargs ->
-         let ce = Declare.definition_entry ~opaque ~types ~univs body in
+  let csts = CList.map2
+      (fun Recthm.{ name; typ; impargs } body ->
+         let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in
          declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
-      fixnames fixdecls fixtypes fiximps
+      fixitems fixdecls
   in
   let isfix = Option.is_empty possible_indexes in
+  let fixnames = List.map (fun { Recthm.name } -> name) fixitems in
   Declare.recursive_message isfix indexes fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   csts
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
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 95e9a10d03..98a9e4b9c9 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -436,7 +436,12 @@ let declare_mutual_definition l =
         (xdef :: defs, xobls @ obls)) l ([], [])
   in
   (*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixdefs, fixrs,fixtypes, fiximps = List.split4 defs in
+  let fixdefs, fixrs, fixtypes, fixitems =
+    List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) ->
+        d :: a1, r :: a2, typ :: a3,
+        DeclareDef.Recthm.{ name; typ; impargs; args = [] } :: a4
+      ) defs first.prg_deps ([],[],[],[])
+  in
   let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in
   let rvec = Array.of_list fixrs in
@@ -449,14 +454,14 @@ let declare_mutual_definition l =
     | IsCoFixpoint -> None
   in
   (* In the future we will pack all this in a proper record *)
-  let poly, scope, ntns, opaque, fixnames = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque, first.prg_deps in
+  let poly, scope, ntns, opaque = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque in
   let kind = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) else Decls.(IsDefinition CoFixpoint) in
   (* Declare the recursive definitions *)
   let udecl = UState.default_univ_decl in
   let kns =
     DeclareDef.declare_mutually_recursive ~scope ~opaque ~kind
-      ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes
-      ~poly ~restrict_ucontext:false fixnames fixtypes fiximps
+      ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
+      ~restrict_ucontext:false fixitems
   in
   (* Only for the first constant *)
   let fix_exn = Hook.get get_fix_exn () in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7782ff8ac9..7aea40c718 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -39,15 +39,6 @@ module Proof_ending = struct
 
 end
 
-module Recthm = struct
-  type t =
-    { name : Id.t
-    ; typ : Constr.t
-    ; args : Name.t list
-    ; impargs : Impargs.manual_implicits
-    }
-end
-
 module Info = struct
 
   type t =
@@ -56,7 +47,7 @@ module Info = struct
     ; impargs : Impargs.manual_implicits
     ; proof_ending : Proof_ending.t CEphemeron.key
     (* This could be improved and the CEphemeron removed *)
-    ; other_thms : Recthm.t list
+    ; other_thms : DeclareDef.Recthm.t list
     ; scope : DeclareDef.locality
     ; kind : Decls.logical_kind
     }
@@ -129,7 +120,7 @@ let start_dependent_lemma ~name ~poly
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun { Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with
+    match List.map (fun { DeclareDef.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -137,12 +128,12 @@ let rec_tac_initializer finite guard thms snl =
     let nl = match snl with
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun { Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
+    in match List.map2 (fun { DeclareDef.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
 let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl =
-  let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
+  let intro_tac { DeclareDef.Recthm.args; _ } = Tactics.auto_intros_tac args in
   let init_tac, compute_guard = match recguard with
   | Some (finite,guard,init_terms) ->
     let rec_tac = rec_tac_initializer finite guard thms snl in
@@ -162,7 +153,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
     intro_tac (List.hd thms), [] in
   match thms with
   | [] -> CErrors.anomaly (Pp.str "No proof to start.")
-  | { Recthm.name; typ; impargs; _}::other_thms ->
+  | { DeclareDef.Recthm.name; typ; impargs; _}::other_thms ->
     let info =
       Info.{ hook
            ; impargs
@@ -290,7 +281,7 @@ end = struct
     let ubind = UnivNames.empty_binders in
     let rs =
       List.map_i (
-        fun i { Recthm.name; typ; impargs } ->
+        fun i { DeclareDef.Recthm.name; typ; impargs } ->
           declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms
     in r :: rs
 end
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 471c955311..6a1f8c09f3 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -44,19 +44,6 @@ module Proof_ending : sig
 
 end
 
-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
-
 module Info : sig
 
   type t
@@ -104,7 +91,7 @@ val start_lemma_with_initialization
   -> udecl:UState.universe_decl
   -> Evd.evar_map
   -> (bool * lemma_possible_guards * Constr.t option list option) option
-  -> Recthm.t list
+  -> DeclareDef.Recthm.t list
   -> int list option
   -> t
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d273573270..8641c67d9f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -501,7 +501,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
   let thms = List.map (fun (name, (typ, (args, impargs))) ->
-      { Lemmas.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
+      { DeclareDef.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
   let () =
     let open UState in
     if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
-- 
cgit v1.2.3


From ec60835e6a41f368c1a91d4eac8c99e1853a2abc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 02:58:28 -0400
Subject: [lemmas] Use direct-style for variable declaration.

Steps towards unification with `DeclareDef` API.
---
 vernac/lemmas.ml | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7aea40c718..95ed3e2a8e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -179,13 +179,20 @@ module MutualEntry : sig
   (* We keep this type abstract and to avoid uncontrolled hacks *)
   type t
 
-  val variable : info:Info.t -> Entries.parameter_entry -> t
-
   val adjust_guardness_conditions
     : info:Info.t
     -> Evd.side_effects Declare.proof_entry
     -> t
 
+  val declare_variable
+    : info:Info.t
+    -> uctx:UState.t
+    (* Only for the first constant, introduced by compat *)
+    -> ubind:UnivNames.universe_binders
+    -> name:Id.t
+    -> Entries.parameter_entry
+    -> Names.GlobRef.t list
+
   val declare_mutdef
     (* Common to all recthms *)
     : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
@@ -210,8 +217,6 @@ end = struct
     ; info : Info.t
     }
 
-  let variable ~info t = { entry = NoBody t; info }
-
   (* XXX: Refactor this with the code in
      [ComFixpoint.declare_fixpoint_generic] *)
   let guess_decreasing env possible_indexes ((body, ctx), eff) =
@@ -284,6 +289,10 @@ end = struct
         fun i { DeclareDef.Recthm.name; typ; impargs } ->
           declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms
     in r :: rs
+
+  let declare_variable ~info ~uctx ~ubind ~name pe =
+    declare_mutdef ~uctx ~ubind ~name { entry = NoBody pe; info }
+
 end
 
 (************************************************************************)
@@ -311,10 +320,8 @@ let compute_proof_using_for_admitted proof typ pproofs =
     | _ -> None
 
 let finish_admitted ~name ~info ~uctx pe =
-  let mutpe = MutualEntry.variable ~info pe in
   let ubind = UnivNames.empty_binders in
-  let _r : Names.GlobRef.t list =
-    MutualEntry.declare_mutdef ~uctx ~ubind ~name mutpe in
+  let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx ~ubind ~name pe in
   ()
 
 let save_lemma_admitted ~(lemma : t) : unit =
@@ -352,9 +359,9 @@ let finish_proved idopt po info =
       | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
     let fix_exn = Declare.Internal.get_fix_exn const in
     let () = try
-      let mutpe = MutualEntry.adjust_guardness_conditions ~info const in
       let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
       let ubind = UState.universe_binders uctx in
+      let mutpe = MutualEntry.adjust_guardness_conditions ~info const in
       let _r : Names.GlobRef.t list =
         MutualEntry.declare_mutdef ~fix_exn ~uctx ?hook_data ~ubind ~name mutpe
       in ()
-- 
cgit v1.2.3


From f52e7e152e37000d081470f73786ccdd9167f1c0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 03:01:40 -0400
Subject: [lemmas] Use direct-style for mutual lemma declaration.

Steps towards unification with `DeclareDef` API.
---
 vernac/lemmas.ml | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 95ed3e2a8e..e08d2ce117 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -176,14 +176,6 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
 (* XXX: Most of this does belong to Declare, due to proof_entry manip *)
 module MutualEntry : sig
 
-  (* We keep this type abstract and to avoid uncontrolled hacks *)
-  type t
-
-  val adjust_guardness_conditions
-    : info:Info.t
-    -> Evd.side_effects Declare.proof_entry
-    -> t
-
   val declare_variable
     : info:Info.t
     -> uctx:UState.t
@@ -195,13 +187,14 @@ module MutualEntry : sig
 
   val declare_mutdef
     (* Common to all recthms *)
-    : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+    : info:Info.t
+    -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
     -> uctx:UState.t
     -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list
     (* Only for the first constant, introduced by compat *)
     -> ubind:UnivNames.universe_binders
     -> name:Id.t
-    -> t
+    -> Evd.side_effects Declare.proof_entry
     -> Names.GlobRef.t list
 
 end = struct
@@ -293,6 +286,10 @@ end = struct
   let declare_variable ~info ~uctx ~ubind ~name pe =
     declare_mutdef ~uctx ~ubind ~name { entry = NoBody pe; info }
 
+  let declare_mutdef ~info ?fix_exn ~uctx ?hook_data ~ubind ~name const =
+    let mutpe = adjust_guardness_conditions ~info const in
+    declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name mutpe
+
 end
 
 (************************************************************************)
@@ -361,9 +358,8 @@ let finish_proved idopt po info =
     let () = try
       let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
       let ubind = UState.universe_binders uctx in
-      let mutpe = MutualEntry.adjust_guardness_conditions ~info const in
       let _r : Names.GlobRef.t list =
-        MutualEntry.declare_mutdef ~fix_exn ~uctx ?hook_data ~ubind ~name mutpe
+        MutualEntry.declare_mutdef ~info ~fix_exn ~uctx ?hook_data ~ubind ~name const
       in ()
     with e when CErrors.noncritical e ->
       let e = Exninfo.capture e in
-- 
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.ml  | 4 ++--
 vernac/declareDef.mli | 4 +++-
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 6e19cf97b0..fc53abdcea 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -95,11 +95,11 @@ module Recthm = struct
     }
 end
 
-let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixitems =
+let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
   let vars, fixdecls, indexes =
     mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
   let ubind, univs =
-    (* XXX: Note that obligations don't do this, is that a bug? *)
+    (* XXX: Obligations don't do this, this seems like a bug? *)
     if restrict_ucontext
     then
       let evd = Evd.from_ctx uctx in
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