X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.mli;h=95ee658c7de98b637cc10261e8b6317efa4d3959;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=1dbcc11c86efecb6bb78bef136d6ecf0ccd9d55f;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
index 1dbcc11c8..95ee658c7 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
@@ -23,21 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
-type type_checker_exn =
-   Impossible of int
- | NotWellTyped of string
- | WrongUriToConstant of string
- | WrongUriToVariable of string
- | WrongUriToMutualInductiveDefinitions of string
- | ListTooShort
- | NotPositiveOccurrences of string
- | NotWellFormedTypeOfInductiveConstructor of string
- | WrongRequiredArgument of string
- | RelToHiddenHypothesis
- | MetasenvInconsistency;;
-
-(* This is the only exception that will be raised *)
-exception TypeCheckerFailure of type_checker_exn;;
+(* These are the only exceptions that will be raised *)
+exception TypeCheckerFailure of string
+exception AssertFailure of string
 
 val typecheck : UriManager.uri -> unit