better exception and error messages

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.mli

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
index 1dbcc11c86efecb6bb78bef136d6ecf0ccd9d55f..d3db80a46a6d951732875ae63deecd8c861bbd3e 100644 (file)
--- 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;;
+exception TypeCheckerFailure of string
+exception AssertFailure of string
 
 val typecheck : UriManager.uri -> unit