| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
|
|
This commit was created via `./dev/tools/update-compat.py --master`
|
|
Reviewed-by: cpitclaudel
|
|
Ack-by: Zimmi48
Ack-by: anton-trunov
Ack-by: jfehrle
|
|
Reviewed-by: Zimmi48
|
|
\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.
|
|
|
|
In particular, add an example to illustrate the associativity of ;
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
Move plugin tutorial to Coq repo
|
|
|
|
|
|
Not sure what the right solution is here, but we can improve after the merge.
|
|
'168a13dab1c9987f592994150997e692d4d7e40b'
git-subtree-dir: doc/plugin_tutorial
git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7
git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b
|
|
|
|
The way to override this default is not exactly the same as in the legacy Makefile
but it has been documented as well.
|
|
|
|
|
|
|
|
|
|
This commit implements the following intro patterns:
Temporary "=> +"
"move=> + stuff" ==== "move=> tmp stuff; move: tmp"
It preserves the original name.
"=>" can be chained to force generalization as in
"move=> + y + => x z"
Tactics as views "=> /ltac:(tactic)"
Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo".
Limited to views on the right of "=>", views that decorate a tactic
as move or case are not supported to be tactics.
Dependent "=> >H"
move=> >H ===== move=> ???? H, with enough ? to
name H the first non-dependent assumption (LHS of the first arrow).
TC isntances are skipped.
Block intro "=> [^ H] [^~ H]"
after "case" or "elim" or "elim/v" it introduces in one go
all new assumptions coming from the eliminations. The names are
picked from the inductive type declaration or the elimination principle
"v" in "elim/v" and are appended/prepended the seed "H"
The implementation makes crucial use of the goal_with_state feature of
the tactic monad. For example + schedules a generalization to be performed
at the end of the intro pattern and [^ .. ] reads the name seeds from
the state (that is filled in by case and elim).
|
|
|
|
Dune.
|
|
|
|
|
|
|
|
interning phase
|
|
This is a reduced version of #8503 as to provide a way to build the
reference manual with Dune.
Dune 1.6 supports (experimentally) directories as targets, thus we
introduce a rule that will call `sphinx` to build the manual.
This only provides build, however generation of `.install` rules is
not done, it will be hopefully addressed in #8503.
Note that we set `expire: 1 month` for all the artifacts we build with
Dune. IMHO this makes most sense as not to abuse Gitlab's hosting,
however of course we could consider a different deployment strategy if
wanted.
|
|
in refman.
|
|
|
|
|
|
|
|
Follow-up of #8987.
|
|
|
|
Also remove a few undocumented settings
|
|
Namely, it does not explicitly open a scope, but we remember that we
don't need the %type delimiter when in type position.
|
|
This modifies the strategy in previous commits so that priorities are
as before in case of non-open scopes with delimiters.
Additionally, we document the rare situation of overlapping
applicative notations (maybe this is too rare and ad hoc to be worth
being documented though).
|
|
Mostly courtesy of Jason Gross.
|
|
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
|
|
|
|
to fix all misuses.
|
|
|
|
And a few more Sphinx fixes in passing.
|
|
As per https://github.com/coq/coq/pull/8965#discussion_r237225852
|
|
As per https://github.com/coq/coq/pull/8965/files#r237225852
|
