X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.mli;h=d3db80a46a6d951732875ae63deecd8c861bbd3e;hb=7cb90c67bc6f8113188a91ecc29f6db20db5aeb8;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..d3db80a46 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;; +exception TypeCheckerFailure of string +exception AssertFailure of string val typecheck : UriManager.uri -> unit