diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-22 15:36:58 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-22 15:36:58 +0000 |
| commit | 10961655cb9c09da20cfe2ecc68def3d3b7d1bb5 (patch) | |
| tree | fe435d1bd014a15e0b430cac8d7fb6bddc75f5e3 /contrib/subtac/subtac_errors.mli | |
| parent | 8291c83620312550d1ccbe9a304fd43f35724b12 (diff) | |
Made pretyping a functor over a coercion implementation. Pretyping.Default uses the original Coercion implementation.
Updated contributions that called pretyping to use the default impl.
Also update subtac using the functor, do some renamings and add interfaces for all files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/subtac_errors.mli')
| -rw-r--r-- | contrib/subtac/subtac_errors.mli | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_errors.mli b/contrib/subtac/subtac_errors.mli new file mode 100644 index 000000000..8d75b9c01 --- /dev/null +++ b/contrib/subtac/subtac_errors.mli @@ -0,0 +1,15 @@ +type term_pp = Pp.std_ppcmds +type subtyping_error = + UncoercibleInferType of Util.loc * term_pp * term_pp + | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp + | UncoercibleRewrite of term_pp * term_pp +type typing_error = + NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp + | NonConvertible of Util.loc * term_pp * term_pp + | NonSigma of Util.loc * term_pp + | IllSorted of Util.loc * term_pp +exception Subtyping_error of subtyping_error +exception Typing_error of typing_error +exception Debug_msg of string +val typing_error : typing_error -> 'a +val subtyping_error : subtyping_error -> 'a |