From f912004bbe2c8f77de09cc290c3c687dc4ebf7f8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 8 May 2014 13:43:26 +0200
Subject: Adapt the checker to polymorphic universes and projections
 (untested).

---
 checker/type_errors.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'checker/type_errors.ml')

diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index e800ee3ef2..565005b908 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -45,7 +45,7 @@ type type_error =
   | NotAType of unsafe_judgment
   | BadAssumption of unsafe_judgment
   | ReferenceVariables of constr
-  | ElimArity of inductive * sorts_family list * constr * unsafe_judgment
+  | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of unsafe_judgment
   | WrongCaseInfo of inductive * case_info
@@ -59,6 +59,7 @@ type type_error =
   | IllFormedRecBody of guard_error * name array * int
   | IllTypedRecBody of
       int * name array * unsafe_judgment array * constr array
+  | UnsatisfiedConstraints of Univ.constraints
 
 exception TypeError of env * type_error
 
@@ -107,4 +108,5 @@ let error_ill_formed_rec_body env why lna i =
 let error_ill_typed_rec_body env i lna vdefj vargs =
   raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs)))
 
-
+let error_unsatisfied_constraints env c =
+  raise (TypeError (env, UnsatisfiedConstraints c))
-- 
cgit v1.2.3