From d5f07aa398419335ec84d609956e39330d8a6a77 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 21 Feb 2024 10:23:17 +0100 Subject: [PATCH] Update doc --- README.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index d6620a80c..f14bdab72 100644 --- a/README.md +++ b/README.md @@ -181,14 +181,13 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`. It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands). - `Elpi Program ` lower level primitive letting one crate a command/tactic with a custom preamble ``. - -- `Elpi Accumulate [] [|File From |Db ]` +- `From some.load.path Extra Dependency "filename" as `. +- `Elpi Accumulate [] [|File |Db ]` adds code to the current program (or `` if specified). The code can be verbatim, from a file or a Db. It understands the `#[skip="rex"]` and `#[only="rex"]` which make the command a no op if the Coq version is matched (or not) by the given regular expression. - File names are relative to the directory mapped to ``; if more than - one such directory exists, the `` must exists only once. + File names `` must have been previously declared with the above command. It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands) - `Elpi Typecheck []` typechecks the current program (or `` if specified).