From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 toplevel/class.ml | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

(limited to 'toplevel/class.ml')

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 3d6d567c..6d53ec9d 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
@@ -32,7 +32,6 @@ type coercion_error_kind =
   | NotAFunction
   | NoSource of cl_typ option
   | ForbiddenSourceClass of cl_typ
-  | NotUniform
   | NoTarget
   | WrongTarget of cl_typ * cl_typ
   | NotAClass of global_reference
@@ -51,9 +50,6 @@ let explain_coercion_error g = function
       (str ": cannot find the source class of " ++ Printer.pr_global g)
   | ForbiddenSourceClass cl ->
       pr_class cl ++ str " cannot be a source class"
-  | NotUniform ->
-      (Printer.pr_global g ++
-         str" does not respect the uniform inheritance condition");
   | NoTarget ->
       (str"Cannot find the target class")
   | WrongTarget (clt,cl) ->
@@ -197,13 +193,13 @@ let build_id_coercion idf_opt source poly =
   let val_f =
     it_mkLambda_or_LetIn
       (mkLambda (Name Namegen.default_dependent_ident,
-		 applistc vs (extended_rel_list 0 lams),
+		 applistc vs (Context.Rel.to_extended_list 0 lams),
 		 mkRel 1))
        lams
   in
   let typ_f =
     it_mkProd_wo_LetIn
-      (mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t))
+      (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list 0 lams), lift 1 t))
       lams
   in
   (* juste pour verification *)
@@ -247,6 +243,12 @@ booleen "coercion identite'?"
 lorque source est None alors target est None aussi.
 *)
 
+let warn_uniform_inheritance =
+  CWarnings.create ~name:"uniform-inheritance" ~category:"typechecker"
+         (fun g ->
+          Printer.pr_global g ++
+            strbrk" does not respect the uniform inheritance condition")
+
 let add_new_coercion_core coef stre poly source target isid =
   check_source source;
   let t = Global.type_of_global_unsafe coef in
@@ -262,7 +264,7 @@ let add_new_coercion_core coef stre poly source target isid =
   in
   check_source (Some cls);
   if not (uniform_cond (llp-ind) lvs) then
-    msg_warning (explain_coercion_error coef NotUniform);
+    warn_uniform_inheritance coef;
   let clt =
     try
       get_target tg ind
@@ -310,7 +312,7 @@ let add_coercion_hook poly local ref =
   in
   let () = try_add_new_coercion ref stre poly in
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
-  Flags.if_verbose msg_info msg
+  Flags.if_verbose Feedback.msg_info msg
 
 let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
 
-- 
cgit v1.2.3