GROS COMMIT:

 - reduction du noyau (variables existentielles, fonctions auxiliaires
   pour inventer des noms, etc. deplacees hors de kernel/)
 - changement de noms de constructeurs des constr (suppression de "Is" et
   "Mut")


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

1 files changed, 35 insertions, 35 deletions

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 05b6e2675..169df5904 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -8,7 +8,6 @@
 
 (* $Id$ *)
 
-open Pp
 open Names
 open Term
 open Sign
@@ -38,68 +37,69 @@ type guard_error =
 type type_error =
   | UnboundRel of int
   | NotAType of unsafe_judgment
-  | BadAssumption of constr
-  | ReferenceVariables of identifier
+  | BadAssumption of unsafe_judgment
+  | ReferenceVariables of constr
   | ElimArity of inductive * constr list * constr * unsafe_judgment
       * (constr * constr * string) option
   | CaseNotInductive of unsafe_judgment
+  | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
   | Generalization of (name * types) * unsafe_judgment
-  | ActualType of constr * constr * constr
+  | ActualType of unsafe_judgment * types
   | CantApplyBadType of (int * constr * constr)
-      * unsafe_judgment * unsafe_judgment list
-  | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list
+      * 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
 
-exception TypeError of path_kind * env * type_error
+exception TypeError of env * type_error
 
 let nfj {uj_val=c;uj_type=ct} =
   {uj_val=c;uj_type=nf_betaiota ct}
 
-let error_unbound_rel k env n =
-  raise (TypeError (k, env, UnboundRel n))
+let error_unbound_rel env n =
+  raise (TypeError (env, UnboundRel n))
 
-let error_not_type k env c =
-  raise (TypeError (k, env, NotAType c))
+let error_not_type env j =
+  raise (TypeError (env, NotAType j))
 
-let error_assumption k env c =
-  raise (TypeError (k, env, BadAssumption c))
+let error_assumption env j =
+  raise (TypeError (env, BadAssumption j))
 
-let error_reference_variables k env id =
-  raise (TypeError (k, env, ReferenceVariables id))
+let error_reference_variables env id =
+  raise (TypeError (env, ReferenceVariables id))
 
-let error_elim_arity k env ind aritylst c pj okinds = 
-  raise (TypeError (k, env, ElimArity (ind,aritylst,c,pj,okinds)))
+let error_elim_arity env ind aritylst c pj okinds = 
+  raise (TypeError (env, ElimArity (ind,aritylst,c,pj,okinds)))
 
-let error_case_not_inductive k env j = 
-  raise (TypeError (k, env, CaseNotInductive j))
+let error_case_not_inductive env j = 
+  raise (TypeError (env, CaseNotInductive j))
 
-let error_number_branches k env cj expn =
-  raise (TypeError (k, env, NumberBranches (nfj cj,expn)))
+let error_number_branches env cj expn =
+  raise (TypeError (env, NumberBranches (nfj cj,expn)))
 
-let error_ill_formed_branch k env c i actty expty =
-  raise (TypeError (k, env,
+let error_ill_formed_branch env c i actty expty =
+  raise (TypeError (env,
     IllFormedBranch (c,i,nf_betaiota actty, nf_betaiota expty)))
 
-let error_generalization k env nvar c =
-  raise (TypeError (k, env, Generalization (nvar,c)))
+let error_generalization env nvar c =
+  raise (TypeError (env, Generalization (nvar,c)))
 
-let error_actual_type k env c actty expty =
-  raise (TypeError (k, env, ActualType (c,actty,expty)))
+let error_actual_type env j expty =
+  raise (TypeError (env, ActualType (j,expty)))
 
-let error_cant_apply_not_functional k env rator randl =
-  raise (TypeError (k, env, CantApplyNonFunctional (rator,randl)))
+let error_cant_apply_not_functional env rator randl =
+  raise (TypeError (env, CantApplyNonFunctional (rator,randl)))
 
-let error_cant_apply_bad_type k env t rator randl =
-  raise(TypeError (k, env, CantApplyBadType (t,rator,randl)))
+let error_cant_apply_bad_type env t rator randl =
+  raise(TypeError (env, CantApplyBadType (t,rator,randl)))
 
-let error_ill_formed_rec_body k env why lna i vdefs =
-  raise (TypeError (k, env, IllFormedRecBody (why,lna,i,vdefs)))
+let error_ill_formed_rec_body env why lna i vdefs =
+  raise (TypeError (env, IllFormedRecBody (why,lna,i,vdefs)))
 
-let error_ill_typed_rec_body k env i lna vdefj vargs =
-  raise (TypeError (k, env, IllTypedRecBody (i,lna,vdefj,vargs)))
+let error_ill_typed_rec_body env i lna vdefj vargs =
+  raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs)))