Skip to content

Commit d5f07aa

Browse files
committed
Update doc
1 parent 3b94c02 commit d5f07aa

File tree

1 file changed

+3
-4
lines changed

1 file changed

+3
-4
lines changed

README.md

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -181,14 +181,13 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
181181
It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
182182
- `Elpi Program <qname> <code>` lower level primitive letting one crate a
183183
command/tactic with a custom preamble `<code>`.
184-
185-
- `Elpi Accumulate [<qname>] [<code>|File <filename> From <loadpath>|Db <dbname>]`
184+
- `From some.load.path Extra Dependency "filename" as <fname>`.
185+
- `Elpi Accumulate [<qname>] [<code>|File <fname>|Db <dbname>]`
186186
adds code to the current program (or `<qname>` if specified).
187187
The code can be verbatim, from a file or a Db.
188188
It understands the `#[skip="rex"]` and `#[only="rex"]` which make the command
189189
a no op if the Coq version is matched (or not) by the given regular expression.
190-
File names are relative to the directory mapped to `<loadpath>`; if more than
191-
one such directory exists, the `<filename>` must exists only once.
190+
File names `<fname>` must have been previously declared with the above command.
192191
It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
193192
- `Elpi Typecheck [<qname>]` typechecks the current program (or `<qname>` if
194193
specified).

0 commit comments

Comments
 (0)