Suites modifs du noyau. Univ devient purement fonctionnel.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 17 deletions

diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index c342ce892..3ffb585c5 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -11,7 +11,6 @@
 (*i*)
 open Names
 open Term
-open Sign
 open Environ
 (*i*)
 
@@ -39,6 +38,7 @@ type guard_error =
 
 type type_error =
   | UnboundRel of int
+  | UnboundVar of variable
   | NotAType of unsafe_judgment
   | BadAssumption of unsafe_judgment
   | ReferenceVariables of constr
@@ -50,17 +50,19 @@ type type_error =
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * types) * unsafe_judgment
   | ActualType of unsafe_judgment * types
-  | CantApplyBadType of (int * constr * constr)
-      * unsafe_judgment * unsafe_judgment array
+  | CantApplyBadType of
+      (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
   | IllFormedRecBody of guard_error * name array * int * constr array
-  | IllTypedRecBody of int * name array * unsafe_judgment array 
-      * types array
+  | IllTypedRecBody of
+      int * name array * unsafe_judgment array * types array
 
 exception TypeError of env * type_error
 
 val error_unbound_rel : env -> int -> 'a
 
+val error_unbound_var : env -> variable -> 'a
+
 val error_not_type : env -> unsafe_judgment -> 'a
 
 val error_assumption : env -> unsafe_judgment -> 'a
@@ -71,20 +73,15 @@ val error_elim_arity :
   env -> inductive -> constr list -> constr 
     -> unsafe_judgment -> (constr * constr * string) option -> 'a
 
-val error_case_not_inductive : 
-  env -> unsafe_judgment -> 'a
+val error_case_not_inductive : env -> unsafe_judgment -> 'a
 
-val error_number_branches : 
-  env -> unsafe_judgment -> int -> 'a
+val error_number_branches : env -> unsafe_judgment -> int -> 'a
 
-val error_ill_formed_branch :
-  env -> constr -> int -> constr -> constr -> 'a
+val error_ill_formed_branch : env -> constr -> int -> constr -> constr -> 'a
 
-val error_generalization :
-  env -> name * types -> unsafe_judgment -> 'a
+val error_generalization : env -> name * types -> unsafe_judgment -> 'a
 
-val error_actual_type :
-  env -> unsafe_judgment -> types -> 'a
+val error_actual_type : env -> unsafe_judgment -> types -> 'a
 
 val error_cant_apply_not_functional : 
   env -> unsafe_judgment -> unsafe_judgment array -> 'a
@@ -97,6 +94,5 @@ val error_ill_formed_rec_body :
   env -> guard_error -> name array -> int -> constr array -> 'a
 
 val error_ill_typed_rec_body  :
-  env -> int -> name array -> unsafe_judgment array 
-    -> types array -> 'a
+  env -> int -> name array -> unsafe_judgment array -> types array -> 'a