diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/README.md | 2 | ||||
| -rw-r--r-- | dev/doc/build-system.txt | 8 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 2 | ||||
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 |
4 files changed, 7 insertions, 7 deletions
diff --git a/dev/README.md b/dev/README.md index 4cda60a703..0c6b8020f1 100644 --- a/dev/README.md +++ b/dev/README.md @@ -28,7 +28,7 @@ | [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine | | [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections | | [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine | -| [`dev/doc/xml-protocol.md`](doc/proof-engine.md) | XML protocol that coqtop and IDEs use to communicate | +| [`dev/doc/xml-protocol.md`](doc/xml-protocol.md) | XML protocol that coqtop and IDEs use to communicate | | [`dev/doc/MERGING.md`](doc/MERGING.md) | How pull requests should be merged into `master` | | [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release | diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index a14781a058..b8987b7086 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -89,7 +89,7 @@ enables partial recalculation of dependencies (only the dependencies of changed files are recomputed). If you add a dependency to a Coq camlp5 extension (grammar.cma or -q_constr.cmo), then see sections ".ml4 files" and "new files". +q_constr.cmo), then see sections ".mlg files" and "new files". Cleaning Targets ---------------- @@ -113,13 +113,13 @@ Targets for cleaning various parts: - docclean: clean documentation -.ml4/.mlp files +.mlg/.mlp files --------------- 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 + - a .mlg is now always preprocessed with grammar.cma (and q_constr.cmo), + except coqide_main.mlg and its specific rule This classification replaces the old mechanism of declaring the use of a grammar extension via a line of the form: diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index e5e4f740bd..096ffe6a1c 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -20,7 +20,7 @@ Special components grammar : Camlp5 syntax extensions. The file grammar/grammar.cma is used - to pre-process .ml4 files containing EXTEND constructions, + to pre-process .mlg files containing EXTEND constructions, either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND. This grammar.cma incorporates many files from other directories (mainly parsing/), plus some specific files in grammar/. diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 601d52ddda..2f5c7128e2 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -727,7 +727,7 @@ Conflicts exists between integers and constrs. \nlsep \TERM{setoid_replace} ~\tacconstr ~\KWD{with} ~\tacconstr \nlsep \TERM{setoid_rewrite} ~\NT{orient} ~\tacconstr \nlsep \TERM{subst} ~\STAR{\NT{ident}} -%% eqdecide.ml4 +%% eqdecide.mlg \nlsep \TERM{decide}~\TERM{equality} ~\OPTGR{\tacconstr~\tacconstr} \nlsep \TERM{compare}~\tacconstr~\tacconstr %% eauto |