Commit 05972a08 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Absence of locations in a goal triggers an exception only in debug mode

parent 6416a393
...@@ -504,7 +504,14 @@ exception No_loc_on_goal ...@@ -504,7 +504,14 @@ exception No_loc_on_goal
let color_goal list loc = let color_goal list loc =
match loc with match loc with
| None -> raise No_loc_on_goal | None ->
(* This case can happen when after some transformations: for example, in
an assert, the new goal asserted is not tagged with locations *)
(* This error is harmless but we want to detect it when debugging. *)
if Debug.test_flag Debug.stack_trace then
raise No_loc_on_goal
| Some loc -> color_loc list ~color:Goal_color ~loc | Some loc -> color_loc list ~color:Goal_color ~loc
let get_locations list (task: Task.task) = let get_locations list (task: Task.task) =
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment