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