diff options
| author | Pierre-Marie Pédrot | 2014-11-20 18:40:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-20 18:41:17 +0100 |
| commit | 2ea61f39331d8ed776aaad2f5a10988d6658ca49 (patch) | |
| tree | 4ab37538f57b1a05da9491d3291baaef9bf98d33 | |
| parent | be3a07eafa86a23f06297a9f971413ecfbe41959 (diff) | |
Adding locations to tclZEROMSG.
| -rw-r--r-- | tactics/tacticals.ml | 9 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 |
2 files changed, 8 insertions, 3 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bc7e5f7cda..97e2373b7e 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -298,8 +298,13 @@ module New = struct let tclFAIL lvl msg = tclZERO (Refiner.FailError (lvl,lazy msg)) - let tclZEROMSG msg = - tclZERO (UserError ("", msg)) + let tclZEROMSG ?loc msg = + let err = UserError ("", msg) in + let err = match loc with + | None -> err + | Some loc -> Loc.add_loc err loc + in + tclZERO err let catch_failerror e = try diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 54aa3b6976..d6630bb79b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -165,7 +165,7 @@ module New : sig THIS MODULE. *) val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic - val tclZEROMSG : Pp.std_ppcmds -> 'a tactic + val tclZEROMSG : ?loc:Loc.t -> Pp.std_ppcmds -> 'a tactic (** Fail with a [User_Error] containing the given message. *) val tclOR : unit tactic -> unit tactic -> unit tactic |