diff options
| author | herbelin | 2005-12-17 21:13:48 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-17 21:13:48 +0000 |
| commit | ae6c95a3755fc3a9434bcc9fdd81b7c69baa8280 (patch) | |
| tree | 695244819d00b4816223e572c7867ca21efa9758 /toplevel | |
| parent | cea2061080d540c0507192eca1887ea4b502680d (diff) | |
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError et suite correction bug #1028
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7660 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 8 | ||||
| -rw-r--r-- | toplevel/himsg.mli | 2 |
3 files changed, 10 insertions, 2 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 913f1250de..8a44877279 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -76,6 +76,8 @@ let rec explain_exn_default = function hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te) | InductiveError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e) + | RecursionSchemeError e -> + hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e) | Cases.PatternMatchingError (env,e) -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 55201ea43d..40fae1e8fd 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -586,8 +586,9 @@ let error_bad_induction dep indid kind = let error_not_mutual_in_scheme () = str "Induction schemes are concerned only with distinct mutually inductive types" +(* Inductive constructions errors *) + let explain_inductive_error = function - (* These are errors related to inductive constructions *) | NonPos (env,c,v) -> error_non_strictly_positive env c v | NotEnoughArgs (env,c,v) -> error_ill_formed_inductive env c v | NotConstructor (env,c,v) -> error_ill_formed_constructor env c v @@ -597,7 +598,10 @@ let explain_inductive_error = function | SameNamesOverlap idl -> error_same_names_overlap idl | NotAnArity id -> error_not_an_arity id | BadEntry -> error_bad_entry () - (* These are errors related to recursors *) + +(* Recursion schemes errors *) + +let explain_recursion_scheme_error = function | NotAllowedCaseAnalysis (dep,k,i) -> error_not_allowed_case_analysis dep k i | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 1c389b9c26..2625243dc9 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -27,6 +27,8 @@ val explain_pretype_error : env -> pretype_error -> std_ppcmds val explain_inductive_error : inductive_error -> std_ppcmds +val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds + val explain_refiner_error : refiner_error -> std_ppcmds val explain_pattern_matching_error : |