| Age | Commit message (Collapse) | Author |
|---|
|
Let vs Definition / Example syntax was split in 7c28130 for parsing
reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could
be introduced. This split is probably the reason why Let was
overlooked when support for universe bindings and universe constraints
were added to Definition and variants.
|
|
|
|
Reviewed-by: Zimmi48
|
|
Fix makefile glitches
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
Use `dune build @check-gram --auto-promote` to automatically update
these two files. You will need to run it twice if the two files need
to be updated (which is the case most often) as Dune will stop after
the first diff failure.
The rst files are also updated but left in the `_build/` directory as
Dune wouldn't support targets outside the current directory. You can
just `mv _build/default/doc/sphinx doc` to update them after running
the @check-gram target.
|
|
Remove unneeded source and output files
Move all commands under command NT
Add a lot of edits for commands and tactics
|
|
|
|
following changes to attribute parsing.
|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
|
|
Show effect of edits to edited nt in PRINT
Add cmdv:: info to prodnCommands
Supporting code globally replaces a given "substring" in productions
with another. (Substring over doc_symbols, not over characters.)
|
|
those in the rsts.
|
|
|
|
Update doc_grammar tool
The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
rsts using instructions embedded in the rsts
Running doc_grammar is currently a manual step.
The grammar updates in the rst files have been manually reviewed.
|
|
for integers and natural nums
|
|
and inserting it into the .rst files
|
