diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 66ba16db6..f2a49e838 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -102,8 +102,9 @@ type existential = int * constr array type constant = section_path * constr array type constructor = constructor_path * constr array type inductive = inductive_path * constr array -type fixpoint = (int array * int) * (constr array * name list * constr array) -type cofixpoint = int * (constr array * name list * constr array) +type rec_declaration = constr array * name list * constr array +type fixpoint = (int array * int) * rec_declaration +type cofixpoint = int * rec_declaration type kind_of_term = |