diff options
| -rw-r--r-- | test-suite/success/ltac.v | 4 | ||||
| -rw-r--r-- | toplevel/ide_blob.ml | 3 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 7 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 5 |
5 files changed, 9 insertions, 13 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index a8d1ba7f5a..7387add6a2 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -298,3 +298,7 @@ evar(foo:nat). let evval := eval compute in foo in not_eq evval 1. let evval := eval compute in foo in not_eq 1 evval. Abort. + +(* Check that this returns an error and not an anomaly (see r13667) *) + +Fail Local Tactic Notation "myintro" := intro. diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index b90b44687c..3bd9462cef 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -529,8 +529,7 @@ type 'a value = let eval_call c = let filter_compat_exn = function - | Vernac.DuringCommandInterp (loc,inner) - | Vernacexpr.DuringSyntaxChecking (loc,inner) -> inner + | Vernac.DuringCommandInterp (loc,inner) -> inner | Vernacexpr.Quit -> raise Vernacexpr.Quit | e -> e in diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 7b3acfa619..ddf3ac6575 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -275,7 +275,6 @@ let rec is_pervasive_exn = function | Error_in_file (_,_,e) -> is_pervasive_exn e | Loc.Exc_located (_,e) -> is_pervasive_exn e | DuringCommandInterp (_,e) -> is_pervasive_exn e - | DuringSyntaxChecking (_,e) -> is_pervasive_exn e | _ -> false (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D @@ -284,8 +283,7 @@ let rec is_pervasive_exn = function let print_toplevel_error exc = let (dloc,exc) = match exc with - | DuringCommandInterp (loc,ie) - | DuringSyntaxChecking (loc,ie) -> + | DuringCommandInterp (loc,ie) -> if loc = dummy_loc then (None,ie) else (Some loc, ie) | _ -> (None, exc) in @@ -334,8 +332,7 @@ let rec discard_to_dot () = * in encountered. *) let process_error = function - | DuringCommandInterp _ - | DuringSyntaxChecking _ as e -> e + | DuringCommandInterp _ as e -> e | e -> if is_pervasive_exn e then e diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 1df58a10ae..2293707e2d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -33,8 +33,7 @@ exception HasNotFailed let raise_with_file file exc = let (cmdloc,re) = match exc with - | DuringCommandInterp(loc,e) - | DuringSyntaxChecking(loc,e) -> (loc,e) + | DuringCommandInterp(loc,e) -> (loc,e) | e -> (dummy_loc,e) in let (inner,inex) = diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 36c2b26c01..797fc79c6c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -351,10 +351,7 @@ and located_vernac_expr = loc * vernac_expr (* Locating errors raised just after the dot is parsed but before the interpretation phase *) -exception DuringSyntaxChecking of exn located - -let syntax_checking_error loc s = - raise (DuringSyntaxChecking (loc,UserError ("",Pp.str s))) +let syntax_checking_error loc s = user_err_loc (loc,"",Pp.str s) (**********************************************************************) (* Managing locality *) |