From 43cbe7053fbd4eb0dff99183a7b869adbca0b061 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Oct 2023 11:40:20 +0200 Subject: [PATCH] fix location for Elpi Accumulate lp:{{ ... }}. --- src/coq_elpi_arg_syntax.mlg | 1 + src/coq_elpi_vernacular_syntax.mlg | 1 + 2 files changed, 2 insertions(+) diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg index d7b54a2f4..acc8d20d0 100644 --- a/src/coq_elpi_arg_syntax.mlg +++ b/src/coq_elpi_arg_syntax.mlg @@ -47,6 +47,7 @@ END GRAMMAR EXTEND Gram GLOBAL: elpi_string; elpi_string : FIRST [ [ s = QUOTATION "lp:" -> { + let loc = { loc with Loc.bp = loc.Loc.bp + 3 } in if s.[0] = '\123' then strip_curly loc s else if s.[0] = '(' then strip_round loc s else if s.[0] = '[' then strip_square loc s diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index a81d1a39a..b83340333 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -66,6 +66,7 @@ GRAMMAR EXTEND Gram term: LEVEL "0" [ [ s = QUOTATION "lp:" -> { + let loc = { loc with Loc.bp = loc.Loc.bp + 3 } in let arg = if s.[0] = '(' then Genarg.in_gen (Genarg.rawwit wit_elpi_code_appArg) (idents_of loc s)