aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-28 11:25:29 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-28 11:25:29 +0200
commit66a68a4329ce199f25184ba8b2d98b4679e7ddae (patch)
treece90c93341c58e82813da8b1a567ce6a3f3ed424 /kernel
parent0a255f51809e8d29a7239bfbd9fe57a8b2b41705 (diff)
parent2ddc9d12bd4616f10245c40bc0c87ae548911809 (diff)
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of let-ins
Diffstat (limited to 'kernel')
-rw-r--r--kernel/constr.ml9
1 files changed, 9 insertions, 0 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 5a7561bf5..e2630c3f0 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -107,7 +107,16 @@ 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