diff options
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 8 |
1 files changed, 8 insertions, 0 deletions
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 |