diff options
Diffstat (limited to 'dev/doc/build-system.txt')
| -rw-r--r-- | dev/doc/build-system.txt | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 31d9875a..873adc1b 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -113,15 +113,20 @@ Targets for cleaning various parts: - docclean: clean documentation -.ml4 files ----------- +.ml4/.mlp files +--------------- -If a .ml4 file uses a grammar extension from Coq (such as grammar.cma -or q_constr.cmo), it must contain a line like: +There is now two kinds of preprocessed files : + - a .mlp do not need grammar.cma (they are in grammar/) + - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), + except coqide_main.ml4 and its specific rule + +This classification replaces the old mechanism of declaring the use +of a grammar extension via a line of the form: (*i camlp4deps: "grammar.cma q_constr.cmo" i*) The use of (*i camlp4use: ... i*) to mention uses of standard -extension such as IFDEF has been discontinued, the Makefile now +extension such as IFDEF has also been discontinued, the Makefile now always calls camlp4 with pa_macros.cmo and a few others by default. For debugging a Coq grammar extension, it could be interesting |