Fixing #7100 (lost of main file location in case of Ltac failure in other file).

1 files changed, 4 insertions, 0 deletions

diff --git a/lib/loc.mli b/lib/loc.mli
index 813c45fbb3..23df1ebd9a 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -42,6 +42,10 @@ val merge : t -> t -> t
 val merge_opt : t option -> t option -> t option
 (** Merge locations, usually generating the largest possible span *)
 
+val finer : t option -> t option -> bool
+(** Answers [true] when the first location is more defined, or, when
+    both defined, included in the second one *)
+
 val shift_loc : int -> int -> t -> t
 (** [shift_loc loc n p] shifts the beginning of location by [n] and
     the end by [p]; it is assumed that the shifts do not change the