From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 kernel/type_errors.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/type_errors.mli')

diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index c56b174b..138c313c 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: type_errors.mli 6019 2004-08-06 18:15:24Z herbelin $ i*)
+(*i $Id: type_errors.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -47,8 +47,8 @@ type type_error =
   | NotAType of unsafe_judgment
   | BadAssumption of unsafe_judgment
   | ReferenceVariables of constr
-  | ElimArity of inductive * types list * constr * unsafe_judgment
-      * (constr * constr * arity_error) option
+  | ElimArity of inductive * sorts_family list * constr * unsafe_judgment
+      * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of unsafe_judgment
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
@@ -75,8 +75,8 @@ val error_assumption : env -> unsafe_judgment -> 'a
 val error_reference_variables : env -> constr -> 'a
 
 val error_elim_arity : 
-  env -> inductive -> types list -> constr 
-    -> unsafe_judgment -> (constr * constr * arity_error) option -> 'a
+  env -> inductive -> sorts_family list -> constr -> unsafe_judgment -> 
+      (sorts_family * sorts_family * arity_error) option -> 'a
 
 val error_case_not_inductive : env -> unsafe_judgment -> 'a
 
-- 
cgit v1.2.3