Merge PR#582: Fix warnings

8 files changed, 12 insertions, 31 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index ae58fd068..eecceb32a 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -987,28 +987,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 =
diff --git a/kernel/names.ml b/kernel/names.ml
index 5c10badbe..811b4a62a 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -542,7 +542,6 @@ module KerPair = struct
   end
 
   module SyntacticOrd = struct
-    type t = kernel_pair
     let compare x y = match x, y with
       | Same knx, Same kny -> KerName.compare knx kny
       | Dual (knux,kncx), Dual (knuy,kncy) ->
@@ -865,7 +864,6 @@ struct
   let hash (c, b) = (if b then 0 else 1) + Constant.hash c
 
   module SyntacticOrd = struct
-    type t = constant * bool
     let compare (c, b) (c', b') =
       if b = b' then Constant.SyntacticOrd.compare c c' else -1
     let equal (c, b as x) (c', b' as x') =
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index d9659d681..ba80ff590 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -16,6 +16,8 @@ open Nativeinstr
 open Nativelambda
 open Pre_env
 
+[@@@ocaml.warning "-32-37"]
+
 (** This file defines the mllambda code generation phase of the native
 compiler. mllambda represents a fragment of ML, and can easily be printed
 to OCaml code. *)
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 366f9a0a6..fcb75c661 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -16,6 +16,9 @@ open Nativeinstr
 
 module RelDecl = Context.Rel.Declaration
 
+(* I'm not messing with this stuff. *)
+[@@@ocaml.warning "-32"]
+
 (** This file defines the lambda code generation phase of the native compiler *)
 
 exception NotClosed
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 965ed67b0..8d5f6388c 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -334,6 +334,7 @@ let l_or accu x y =
   if is_int x && is_int y then no_check_l_or x y
   else accu x y
 
+[@@@ocaml.warning "-37"]
 type coq_carry = 
   | Caccu of t
   | C0 of t
@@ -430,7 +431,7 @@ let addmuldiv accu x y z =
   if is_int x && is_int y && is_int z then no_check_addmuldiv x y z
   else accu x y z
 
-
+[@@@ocaml.warning "-34"]
 type coq_bool =
   | Baccu of t
   | Btrue
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cd975ee9a..ba714ada2 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -487,14 +487,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
         if eq_ind ind1 ind2
 	then
-	  (let cuniv = convert_instances false u1 u2 cuniv in
+	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
              convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
         else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
 	if Int.equal j1 j2 && eq_ind ind1 ind2
 	then
-	  (let cuniv = convert_instances false u1 u2 cuniv in
+	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
         else raise NotConvertible
 	  
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e95cf4d1c..c8ac7df5c 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -61,3 +61,6 @@ val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
 val dump_universes :
   (constraint_type -> string -> string -> unit) ->
   universes -> unit
+
+(** {6 Debugging} *)
+val check_universes_invariants : universes -> unit
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 09f884ecd..afe9cbe8d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -440,10 +440,6 @@ struct
     let set = make Level.set
     let type1 = hcons (Level.set, 1)
 
-    let is_prop = function
-      | (l,0) -> Level.is_prop l
-      | _ -> false
-	
     let is_small = function
       | (l,0) -> Level.is_small l
       | _ -> false