diff options
Diffstat (limited to 'plugins/subtac/subtac_errors.ml')
| -rw-r--r-- | plugins/subtac/subtac_errors.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml index 3bbfe22bc0..067da150ec 100644 --- a/plugins/subtac/subtac_errors.ml +++ b/plugins/subtac/subtac_errors.ml @@ -4,12 +4,12 @@ open Printer type term_pp = Pp.std_ppcmds -type subtyping_error = +type subtyping_error = | UncoercibleInferType of loc * term_pp * term_pp | UncoercibleInferTerm of loc * term_pp * term_pp * term_pp * term_pp | UncoercibleRewrite of term_pp * term_pp -type typing_error = +type typing_error = | NonFunctionalApp of loc * term_pp * term_pp * term_pp | NonConvertible of loc * term_pp * term_pp | NonSigma of loc * term_pp @@ -17,7 +17,7 @@ type typing_error = exception Subtyping_error of subtyping_error exception Typing_error of typing_error - + exception Debug_msg of string let typing_error e = raise (Typing_error e) |