From 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 21 May 2018 21:48:00 +0200
Subject: [kernel] Compile with almost all warnings enabled.

This is a partial resurrection of #6423 but only for the kernel.

IMHO, we pay a bit of price for this but it is a good safety
measure.

Only warning "4: fragile pattern matching" and "44: open hides a type"
are disabled.

We would like to enable 44 for sure once we do some alias cleanup.
---
 kernel/subtyping.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'kernel/subtyping.ml')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 74042f9e04..bfe68671a2 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -138,7 +138,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
   let check_inductive_type cst name t1 t2 =
     check_conv (NotConvertibleInductiveField name)
-      cst (inductive_is_polymorphic mib1) infer_conv_leq env t1 t2
+      cst (inductive_is_polymorphic mib1) (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2
   in
 
   let check_packet cst p1 p2 =
@@ -162,10 +162,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 	cst
   in
   let mind = MutInd.make1 kn1 in
-  let check_cons_types i cst p1 p2 =
+  let check_cons_types _i cst p1 p2 =
     Array.fold_left3
       (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst
-	(inductive_is_polymorphic mib1) infer_conv env t1 t2)
+        (inductive_is_polymorphic mib1) (infer_conv ?l2r:None ?evars:None ?ts:None) env t1 t2)
       cst
       p2.mind_consnames
       (arities_of_specif (mind, inst) (mib1, p1))
@@ -229,7 +229,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
   let check_conv cst poly f = check_conv_error error cst poly f in
   let check_type poly cst env t1 t2 =
     let err = NotConvertibleTypeField (env, t1, t2) in
-    check_conv err cst poly infer_conv_leq env t1 t2
+    check_conv err cst poly (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2
   in
   match info1 with
     | Constant cb1 ->
@@ -268,14 +268,14 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
 		 Anyway [check_conv] will handle that afterwards. *)
 	      let c1 = Mod_subst.force_constr lc1 in
 	      let c2 = Mod_subst.force_constr lc2 in
-	      check_conv NotConvertibleBodyField cst poly infer_conv env c1 c2))
-   | IndType ((kn,i),mind1) ->
+              check_conv NotConvertibleBodyField cst poly (infer_conv ?l2r:None ?evars:None ?ts:None) env c1 c2))
+   | IndType ((_kn,_i),_mind1) ->
        CErrors.user_err Pp.(str @@
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by an inductive type. Hint: you can rename the " ^
        "inductive type and give a definition to map the old name to the new " ^
        "name.")
-   | IndConstr (((kn,i),j),mind1) ->
+   | IndConstr (((_kn,_i),_j),_mind1) ->
       CErrors.user_err Pp.(str @@
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
-- 
cgit v1.2.3