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