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.
---
 kernel/constr.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'kernel/constr.ml')

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


From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 kernel/constr.ml | 22 ----------------------
 1 file changed, 22 deletions(-)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 5a7561bf50..71efe90322 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -978,28 +978,6 @@ module Hcaseinfo = Hashcons.Make(CaseinfoHash)
 
 let case_info_hash = CaseinfoHash.hash
 
-module Hsorts =
-  Hashcons.Make(
-    struct
-      open Sorts
-
-      type t = Sorts.t
-      type u = universe -> universe
-      let hashcons huniv = function
-          Prop c -> Prop c
-        | Type u -> Type (huniv u)
-      let eq s1 s2 =
-        s1 == s2 ||
-	  match (s1,s2) with
-            (Prop c1, Prop c2) -> c1 == c2
-          | (Type u1, Type u2) -> u1 == u2
-          |_ -> false
-      let hash = function
-	| Prop Null -> 0 | Prop Pos -> 1
-	| Type u -> 2 + Universe.hash u
-    end)
-
-(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *)
 let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind
 
 let hcons =
-- 
cgit v1.2.3


From 5365971dfdf4136586527aa4f4c85fbfebeee0bd Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 15:00:56 +0200
Subject: Fix for bug 5507. Mispelt de Bruijn.

---
 kernel/constr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index e2630c3f08..49e17d74d5 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -124,7 +124,7 @@ type types = constr
 (* Term constructors *)
 (*********************)
 
-(* Constructs a DeBrujin index with number n *)
+(* Constructs a DeBruijn index with number n *)
 let rels =
   [|Rel  1;Rel  2;Rel  3;Rel  4;Rel  5;Rel  6;Rel  7; Rel  8;
     Rel  9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|]
-- 
cgit v1.2.3


From d0252cac3167ef1e5cd26c1b9b40aea06d343413 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 17:48:57 +0200
Subject: More consistent writing of de Bruijn.

---
 kernel/constr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 49e17d74d5..ae58fd068b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -124,7 +124,7 @@ type types = constr
 (* Term constructors *)
 (*********************)
 
-(* Constructs a DeBruijn index with number n *)
+(* Constructs a de Bruijn index with number n *)
 let rels =
   [|Rel  1;Rel  2;Rel  3;Rel  4;Rel  5;Rel  6;Rel  7; Rel  8;
     Rel  9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|]
-- 
cgit v1.2.3