| Age | Commit message (Collapse) | Author |
|---|
|
After #8655
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
|
|
Fixes #9418
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes
|
|
Reviewed-by: ejgallego
Ack-by: ppedrot
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
|
|
shortening a strict prefix of an application
Reviewed-by: ejgallego
|
|
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
|
|
|
|
|
|
Reviewed-by: maximedenes
|
|
In response to review comments by Zimmi48
|
|
This commit was created via `./dev/tools/update-compat.py --master`
|
|
We now support --master and --release. On the master branch, we support
four compatibility versions, while on releases and release branches, we
support only three compatibility versions.
We also support --git-add to automatically run `git add` with new and
updated files, and to run `git rm` with deleted files.
|
|
The definition of \plus and \tri in cic.rst is not effective
for HTML output.
So, move them into refman-preamble.sty.
Also, \tri is renamed to \trii to express
the suffix of "\triangleright_\iota".
|
|
Reviewed-by: cpitclaudel
|
|
|
|
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
|
|
Ack-by: Zimmi48
Ack-by: anton-trunov
Ack-by: jfehrle
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Coq and the Coq libraries can now be excluded
(by setting the NOCOQ environment variable).
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: mattam82
Ack-by: ppedrot
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
\nO, \nS, \evenO, \evenS, \oddS, \length, \Nil and \cons are used.
don't use \kw in \kw{n} in Fixpoint typing rule section.
|
|
Fix small errors in cic.rst:
* 3.4.1 Free variables: use :math: for "∀ x:T,~U".
:g: doesn't show "∀" in PDF.
"λx:T.~U" is also changed to :math: to use consistent font.
* 3.4.3 Zeta: ":U" added in "let x:=u:U in t" to be valid let-in expression.
* 3.4.3 convertibility: add :math: for u_2' to apply math formatting.
* 3.4.4.6: fix index. "n" should be "k" because they corresponds k-th
constructor.
* 3.4.5 Type constructor: I changed the section title "Type constructor" to
"Type of constructor".
"Type constructor" means a feature to construct new type.
But this section describes about a type of constructor.
* 3.4.5 Example nattree: The reason of
"``nattree`` occurs only strictly positively in ``A``" should be
bullet 1 instead of bullet 3.
The bullet 3 of strict positivity definition is about product, "∀x ∶ U , V",
but "A" is not a product.
* 3.4.5 Destructors: use :math: for "∀".
:g: doesn't show "∀" in PDF.
Also, :math: is used for expressions which has no "∀" character
for font consistency.
Note that I use \kw{has}\_\kw{length} instead of
\kw{has\_length} because the latter is formatted as has\_length in HTML.
(the backslash is retained.)
* 3.4.5 list example: curly braces added.
* 3.4.5 Fixpoint definition: add :math: for Γ_i to apply math formatting.
* 3.4.6 2nd rule of First abstracting property: use \subst.
This adds a curly brace.
Also, spacing and fonts are adjusted as follows.
* 3.4.1 let-in term: use :math: for variable x, consistent with other term
descriptions.
* 3.4.1 let-in term: use \letin command for concrete let-in term.
* 3.4.2 Note: insert spaces as ((λ x:T.~u)~t).
Since T is more closely reated to x than u, T should be positioned
close to x than u.
Since it seems most application has a space, I inserted a space here
for consistency.
* 3.4.3 beta-reduction: insert spaces as 3.4.2.
* 3.4.3 eta-expansion: insert spaces as 3.4.2.
* 3.4.5 Example: use sans-serif fonts for constructor "O" and "S".
* 3.4.5 Fixpoint definition: insert spaces around "with".
* 3.4.5 Fixpoint typing rule: fix fonts for "O" and "S" as 3.4.5 and
insert spaces as 3.4.2.
* 3.4.5 Fixpoint reduction rule: insert a space between {F} and a_1 for
consistency.
* 3.4.6 First abstracting property: insert spaces as 3.4.2.
|
|
The previous language makes it seem as if record parameters are automatically set as implicit for the projection functions, but (per discussion with @jasongross) the omission of parameters from primitive projection only takes effect in Coq's internal AST.
|
|
the intros tactic to its own subsection. Add grammar and examples.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: MSoegtropIMC
|
|
Ack-by: SkySkimmer
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
|
|
an error
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
computed
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
|
