From 799aed40f4ad80344280735720673ce05b308e1f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 19 Jul 2024 11:34:38 +0200 Subject: [PATCH] Do not escape quotes in verbatim LPDoc documentation. This confuses my text editor and I think this is actually useless. Indeed, looking at the code of Elpi seems to indicate that we do not need one additional level of escaping there. --- src/coq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 353acca99..1162d041b 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1507,7 +1507,7 @@ let coq_locate_builtins = % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%|}; LPDoc "-- Environment: names -----------------------------------------------"; LPDoc {|To make the API more precise we use different data types for the names of global objects. -Note: [ctype \"bla\"] is an opaque data type and by convention it is written [@bla].|}; +Note: [ctype "bla"] is an opaque data type and by convention it is written [@bla].|}; MLData constant; MLData inductive;