From 34d8de84ceb853c98bc80a0623f9afeae317d75f Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:25:49 +0200 Subject: Locally disable some warnings. --- kernel/nativecode.ml | 2 ++ kernel/nativelambda.ml | 3 +++ kernel/nativevalues.ml | 3 ++- 3 files changed, 7 insertions(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d9659d6813..ba80ff590d 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 366f9a0a6d..fcb75c661e 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 965ed67b07..8d5f6388cb 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 -- cgit v1.2.3 From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:36:45 +0200 Subject: Fix omitted labels in function calls --- kernel/reduction.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index cd975ee9a9..ba714ada20 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 -- cgit v1.2.3 From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:04:58 +0200 Subject: Remove some unused values and types --- kernel/names.ml | 2 -- kernel/uGraph.mli | 3 +++ kernel/univ.ml | 4 ---- 3 files changed, 3 insertions(+), 6 deletions(-) (limited to 'kernel') diff --git a/kernel/names.ml b/kernel/names.ml index 5c10badbec..811b4a62a5 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/uGraph.mli b/kernel/uGraph.mli index e95cf4d1cb..c8ac7df5c6 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 09f884ecd0..afe9cbe8d5 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 -- 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') 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