From f14b6f1a17652566f0cbc00ce81421ba0684dad5 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 27 Jun 2016 11:03:43 +0200
Subject: errors.ml renamed into cErrors.ml (avoid clash with an OCaml
 compiler-lib module)

 For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
---
 checker/subtyping.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'checker/subtyping.ml')

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 46d21f6ccb..7eae9b8310 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (*i*)
-open Errors
+open CErrors
 open Util
 open Names
 open Cic
@@ -302,7 +302,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		let c2 = force_constr lc2 in
 		check_conv conv env c1 c2))
       | IndType ((kn,i),mind1) ->
-	  ignore (Errors.error (
+	  ignore (CErrors.error (
 		    "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 " ^
@@ -313,7 +313,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
-      ignore (Errors.error (
+      ignore (CErrors.error (
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
-- 
cgit v1.2.3