diff options
author | SimonBoulier <simon.boulier@ens-rennes.fr> | 2018-05-30 11:33:37 +0200 |
---|---|---|
committer | SimonBoulier <simon.boulier@ens-rennes.fr> | 2018-06-05 15:54:12 +0200 |
commit | b0dee52bfa97405adc7c0dbffa0f3558f349659e (patch) | |
tree | 673c1cbbb05521972da10945d184c1585dd3f8b4 /kernel/constr.ml | |
parent | 00a01f65be79bef8592928941646750968dbe648 (diff) |
Define rec_declaration in terms of prec_declaration.
And similarly for fixpoint and cofixpoint.
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r-- | kernel/constr.ml | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index c11b9ebf4..418229330 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -107,21 +107,13 @@ type t = (t, t, Sorts.t, Instance.t) kind_of_term type constr = t type existential = existential_key * constr array -type rec_declaration = Name.t array * constr array * constr array -type fixpoint = (int array * int) * rec_declaration - (* The array of [int]'s tells for each component of the array of - mutual fixpoints the number of lambdas to skip before finding the - recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) - (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is - the recursive argument); - The second component [int] tells which component of the block is - returned *) -type cofixpoint = int * rec_declaration - (* The component [int] tells which component of the block of - cofixpoint is returned *) type types = constr +type rec_declaration = (constr, types) prec_declaration +type fixpoint = (constr, types) pfixpoint +type cofixpoint = (constr, types) pcofixpoint + (*********************) (* Term constructors *) (*********************) |