diff options
| author | filliatr | 2000-12-15 14:26:58 +0000 |
|---|---|---|
| committer | filliatr | 2000-12-15 14:26:58 +0000 |
| commit | d608222a594861efbae01e71018b8dcfc143e09a (patch) | |
| tree | dbcd4e2ac871b95c15471de3939873bc3684b7e7 /toplevel/errors.ml | |
| parent | 7872cda8545ba82827d34e6940b83f5809990f9d (diff) | |
- suppression mind_extract_params
- contraintes univers parametres inductifs prises en compte
- exception UniverseInconsistency donne un message
"Error: Universe Inconsistency"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1125 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/errors.ml')
| -rw-r--r-- | toplevel/errors.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/errors.ml b/toplevel/errors.ml index c72f2ddb3c..6c76e5e888 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -55,6 +55,8 @@ let rec explain_exn_default = function hOV 0 [< 'sTR "Anomaly: Invalid argument "; 'sTR (guill s); report () >] | Sys.Break -> hOV 0 [< 'fNL; 'sTR"User Interrupt." >] + | Univ.UniverseInconsistency -> + hOV 0 [< 'sTR "Error: Universe Inconsistency." >] | TypeError(k,ctx,te) -> hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error k ctx te >] | InductiveError e -> |