diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 02:22:59 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 06:05:40 -0400 |
| commit | a15e584571a4e153e98a11c93d12759c45ea2dcd (patch) | |
| tree | ecb28582eef51f801e2440f715715dda1b6bb06b /vernac/declareDef.mli | |
| parent | affb6ac843380e8e134fd89380746f2f6f8c11de (diff) | |
[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.
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 21 |
1 files changed, 7 insertions, 14 deletions
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 |