diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 02:09:03 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 06:04:29 -0400 |
| commit | affb6ac843380e8e134fd89380746f2f6f8c11de (patch) | |
| tree | f66eb970c747c1f03a3c5fec6c7c2aaeb1d0a0b8 /vernac/declareDef.mli | |
| parent | 09d6197bd11ed4a323b335118ae749d7caefeb55 (diff) | |
[proof] [mutual] Factorize mutual body construction.
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 |