summaryrefslogtreecommitdiff
path: root/src/latex.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/latex.ml')
-rw-r--r--src/latex.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/latex.ml b/src/latex.ml
index 1806da47..aa786b83 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -300,7 +300,7 @@ let rec read_lines in_chan = function
l :: ls
let latex_loc no_loc l =
- match simp_loc l with
+ match Reporting.simp_loc l with
| Some (p1, p2) ->
begin
let open Lexing in