diff options
| author | delahaye | 2001-04-14 03:16:59 +0000 |
|---|---|---|
| committer | delahaye | 2001-04-14 03:16:59 +0000 |
| commit | 2d8cbed59f1bafb68f188d055138d3c7d02d9e37 (patch) | |
| tree | 7a68ad09007ebed0a76dcf96a54e5cac2b1263a2 | |
| parent | 95d14fc74fd9be10e01a595fb1b23b9fd3984713 (diff) | |
Reparation du bug de Try
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1591 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/logic.ml | 7 | ||||
| -rw-r--r-- | proofs/refiner.ml | 1 | ||||
| -rw-r--r-- | toplevel/errors.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index b06f16682c..e26733a15d 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -60,10 +60,9 @@ exception RefinerError of refiner_error let catchable_exception = function | Util.UserError _ | TypeError _ | RefinerError _ - | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _)) -> - true - | _ -> - false + | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ | + Nametab.GlobalizationError _)) -> true + | _ -> false let error_cannot_unify k (m,n) = raise (RefinerError (CannotUnify (m,n))) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 8e358adea2..eb7118398e 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -432,6 +432,7 @@ let tclORELSE0 t1 t2 g = t1 g with | e when catchable_exception e -> t2 g + | _ -> failwith "ICI!" | FailError lvl -> if lvl = 0 then t2 g diff --git a/toplevel/errors.ml b/toplevel/errors.ml index 3c18bf619e..11e7c38ccd 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -67,7 +67,7 @@ let rec explain_exn_default = function hOV 0 [< 'sTR "Error: Universe Inconsistency." >] | TypeError(k,ctx,te) -> hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error k ctx te >] - | PretypeError(ctx,te) -> + | PretypeError(ctx,te) -> hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_pretype_error ctx te >] | InductiveError e -> hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_inductive_error e >] |