diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-11 20:11:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-11 20:11:01 +0000 |
| commit | 2d9aa9c7f84c3a48c870c354cb1a794e7423db50 (patch) | |
| tree | 78d2611d96105d62ca96615443f7103bb9b4b56e | |
| parent | 487042107e8d7f3fd0350ade726e11d9ba4b6214 (diff) | |
Nouveau type rec_declaration
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@699 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | kernel/term.ml | 11 | ||||
| -rw-r--r-- | kernel/term.mli | 5 |
2 files changed, 10 insertions, 6 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index a450e61b7..b70bb05a0 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -54,8 +54,9 @@ type existential = existential_key * 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 = | IsRel of int @@ -116,8 +117,9 @@ and existential = existential_key * constr array and constant = section_path * constr array and constructor = constructor_path * constr array and inductive = inductive_path * constr array -and fixpoint = (int array * int) * (constr array * name list * constr array) -and cofixpoint = int * (constr array * name list * constr array) +and rec_declaration = constr array * name list * constr array +and fixpoint = (int array * int) * rec_declaration +and cofixpoint = int * rec_declaration and kind_of_term = | IsRel of int @@ -288,6 +290,7 @@ type existential = Internal.existential type constant = Internal.constant type constructor = Internal.constructor type inductive = Internal.inductive +type rec_declaration = Internal.rec_declaration type fixpoint = Internal.fixpoint type cofixpoint = Internal.cofixpoint 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 = |