From c3d6651262a3ef8651de0c738e88b0f8ed34fdc2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 10 Feb 2015 19:32:16 +0100
Subject: Fix typeops ignoring results of check functions with let _, and one
 safety hole in judge_of_constant_knowing parameters which was not checking
 the result of the check correctly (the rest of the calls in that file and all
 of the checker have been checked).

---
 kernel/typeops.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 2642b1867d..48dbacf1a4 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -153,13 +153,13 @@ let type_of_constant_type_knowing_parameters env t paramtyps =
 
 let type_of_constant_knowing_parameters env cst paramtyps =
   let cb = lookup_constant (fst cst) env in
-  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ty, cu = constant_type env cst in
     type_of_constant_type_knowing_parameters env ty paramtyps, cu
 
 let type_of_constant_knowing_parameters_in env cst paramtyps =
   let cb = lookup_constant (fst cst) env in
-  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ty = constant_type_in env cst in
     type_of_constant_type_knowing_parameters env ty paramtyps
 
@@ -171,14 +171,14 @@ let type_of_constant env cst =
 
 let type_of_constant_in env cst =
   let cb = lookup_constant (fst cst) env in
-  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ar = constant_type_in env cst in
     type_of_constant_type_knowing_parameters env ar [||]
 
 let judge_of_constant_knowing_parameters env (kn,u as cst) args =
   let c = mkConstU cst in
   let ty, cu = type_of_constant_knowing_parameters env cst args in
-  let _ = Environ.check_constraints cu env in
+  let () = check_constraints cu env in
     make_judge c ty
 
 let judge_of_constant env cst =
@@ -372,7 +372,7 @@ let judge_of_case env ci pj cj lfj =
   let (pind, _ as indspec) =
     try find_rectype env cj.uj_type
     with Not_found -> error_case_not_inductive env cj in
-  let _ = check_case_info env pind ci in
+  let () = check_case_info env pind ci in
   let (bty,rslty) =
     type_case_branches env indspec pj cj.uj_val in
   let () = check_branch_types env pind cj (lfj,bty) in
-- 
cgit v1.2.3


From e8af74ad7913773c4dfb688167b15b6e15e4397a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 Feb 2015 19:50:19 +0100
Subject: Clarifying the implementation of universe hashconsing.

---
 kernel/univ.ml | 33 ++++++++++++++++-----------------
 1 file changed, 16 insertions(+), 17 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 492762df39..ea57276208 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -233,27 +233,26 @@ module Level = struct
 
   let hash x = x.hash
 
-  let hcons x = 
-    let data' = RawLevel.hcons x.data in
-      if data' == x.data then x
-      else { x with data = data' }
-
   let data x = x.data
 
   (** Hashcons on levels + their hash *)
 
-  let make =
-    let module Self = struct
-      type _t = t
-      type t = _t
-      let equal = equal
-      let hash = hash
-    end in
-    let module WH = Weak.Make(Self) in
-    let pool = WH.create 4910 in fun x ->
-    let x = { hash = RawLevel.hash x; data = x } in
-    try WH.find pool x
-    with Not_found -> WH.add pool x; x
+  module Self = struct
+    type _t = t
+    type t = _t
+    type u = raw_level -> raw_level
+    let equal x y = x.hash == y.hash && x.data == y.data
+    let hash x = x.hash
+    let hashcons hraw x =
+      let data' = hraw x.data in
+      if x.data == data' then x else { x with data = data' }
+  end
+
+  let hcons =
+    let module H = Hashcons.Make(Self) in
+    Hashcons.simple_hcons H.generate H.hcons RawLevel.hcons
+
+  let make l = hcons { hash = RawLevel.hash l; data = l }
 
   let set = make Set
   let prop = make Prop
-- 
cgit v1.2.3


From ac65eef8bbc2e405f1964f35c6a129dfa1755888 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Feb 2015 17:06:13 +0100
Subject: Fixing bug #4019, and checker blow-up at once.

---
 kernel/univ.ml | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index ea57276208..763c0822f2 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -194,7 +194,17 @@ struct
     | Level _, _ -> -1
     | _, Level _ -> 1
     | Var n, Var m -> Int.compare n m
-      
+
+  let hequal x y =
+    x == y ||
+      match x, y with
+      | Prop, Prop -> true
+      | Set, Set -> true
+      | Level (n,d), Level (n',d') ->
+        n == n' && d == d'
+      | Var n, Var n' -> n == n'
+      | _ -> false
+
   let hcons = function
     | Prop as x -> x
     | Set as x -> x
@@ -240,17 +250,17 @@ module Level = struct
   module Self = struct
     type _t = t
     type t = _t
-    type u = raw_level -> raw_level
-    let equal x y = x.hash == y.hash && x.data == y.data
+    type u = unit
+    let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
     let hash x = x.hash
-    let hashcons hraw x =
-      let data' = hraw x.data in
+    let hashcons () x =
+      let data' = RawLevel.hcons x.data in
       if x.data == data' then x else { x with data = data' }
   end
 
   let hcons =
     let module H = Hashcons.Make(Self) in
-    Hashcons.simple_hcons H.generate H.hcons RawLevel.hcons
+    Hashcons.simple_hcons H.generate H.hcons ()
 
   let make l = hcons { hash = RawLevel.hash l; data = l }
 
-- 
cgit v1.2.3