X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.mli;h=1dbcc11c86efecb6bb78bef136d6ecf0ccd9d55f;hb=458d0fc95ae3f3a20bd91e3e29ddeb92a009d0fa;hp=4a7fe8db09399b4b3ecacb416635620453c37091;hpb=30ad9beff172b797049b772e0a710c466c9ed18a;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
index 4a7fe8db0..1dbcc11c8 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
@@ -23,14 +23,21 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotWellTyped of string
-exception WrongUriToConstant of string
-exception WrongUriToVariable of string
-exception WrongUriToMutualInductiveDefinitions of string
-exception ListTooShort
-exception NotPositiveOccurrences of string
-exception NotWellFormedTypeOfInductiveConstructor of string
-exception WrongRequiredArgument of string
+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;;
 
 val typecheck : UriManager.uri -> unit