From 8d69323dff6e1afd17a13dfa8a980e76acb44cdc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 15:53:35 +0200
Subject: Documenting how the recursive indices of a fixpoint are computed.

Also documenting how the implicit arguments by position are computed.
---
 intf/constrexpr.mli | 2 +-
 kernel/constr.ml    | 9 +++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 49bafadc8e..a4a6eb9092 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -19,7 +19,7 @@ open Decl_kinds
 type notation = string
 
 type explicitation =
-  | ExplByPos of int * Id.t option
+  | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
   | ExplByName of Id.t
 
 type binder_kind =
diff --git a/kernel/constr.ml b/kernel/constr.ml
index ce20751abc..d0c580d138 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
 
-- 
cgit v1.2.3