| Age | Commit message (Collapse) | Author |
|---|
|
This feature makes it possible to tell type inference to type
applications of a global `foo` using typing information from the context
once the `n` first arguments are known.
The syntax is: `Arguments foo x y | z`.
Closes #7910
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ggonthier
Reviewed-by: herbelin
Ack-by: jfehrle
Reviewed-by: mattam82
|
|
* use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns,
rather than infix `|`, making pattern syntax consistent with term
syntax.
* disable extending `pattern` grammar with notation incompatible with
the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p
| q)` divisibility notation used by `Numbers`.
* emit a (disabled by default) `disj-pattern-notation` warning when such
`Notation` is attempted.
* update documentation accordingly; document incompatibilities in
`changelog`.
* comment special treatment of `(num)` in grammar.
* update file extensions in `Pcoq` header comment.
* correct the keyword declarations to reflect the contents of the
grammar files; perhaps there should be an option to disable implicit
keyword extension in a `.mlg` file, so that these lists could actually
be checked.
* parse the `|}` manifest record terminator as `|` followed by `}`,
eliminating the `|}` token which conflicts with notations that use `|`
as a terminator (such as, absolute value, norm, or cardinal in
MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator,
`bar_cbrace` rule checks for contiguous symbols, this change entails no
visible behaviour change.
|
|
Progress towards #9411, extracted from #10118, rebased ontop of #10192.
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
notations
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
Closes GH-8482.
|
|
|
|
|
|
The numerals lexed are now [0-9][0-9_]* ([.][0-9_]+)? ([eE][+-]?[0-9][0-9_]*)?
|
|
|
|
|
|
Co-Authored-By: gshen42 <gan.shen@outlook.com>
|
|
|
|
- Refine some `@term` into `@type`
|
|
- Refine some `@term` into `@type`
|
|
- Put "Section mechanism" example earlier
|
|
|
|
- More consistent code indentation
- Nest command variants properly
- Make `Context` explanation a bit less terse, with more links
- Typesetting bits, add some :cmd: links
|
|
|
|
|
|
|
|
|
|
Fix semantic conflict between #9389 and #9654.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jashug
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: vbgl
Reviewed-by: cpitclaudel
|
|
This is intended to be separate from handling of implicit binders.
The remaining uses of declare_manual_implicits satisfy a lot of
assertions, giving the possibility of simplifying the interface in the
future.
Two disabled warnings are added for things that currently pass silently.
Currently only Mtac passes non-maximal implicits to
declare_manual_implicits with the force-usage flag set. When implicit
arguments don't have to be named, should move Mtac over to
set_implicits.
|
|
By default Coq warnings are made fatal when building the manual.
If you want to show a command resulting in a warning, use the warn
option.
Preexisting warnings are either fixed or marked as expected.
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
|
|
The conclusion of W-Ind,
"\WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ}", is changed to
"\WF{E;~\ind{p}{Γ_I}{Γ_C}}{}" because
local contexts should be empty when
inductive definition is defined globally.
This is consistent with W-Global-Assum and W-Global-Def.
The side condition "c_i ∉ Γ ∪ E" which I changed previous commit is
changed again to "c_i ∉ E" because I guess that it tries to
avoid name conflicts to the local contexts in the conclusion.
However, the condition is useless after the local contexts is empty.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
binders.
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
Mostly in the pattern
~~~
.. coqtop:: in
Theorem foo : bla.
Theorem bar : blah. (* nested proof error *)
~~~
|
|
|
|
Also quoted parts are emphasized as coq-8.7.2-reference-manual.pdf.
And two "x:T" are quoted.
|
|
Use LEFT DOUBLE QUOTATION MARK (U+201C) and
RIGHT DOUBLE QUOTATION MARK (U+201D) instead of
QUOTATION MARK (U+0022).
QUOTATION MARK is formatted as same form both for
opening and closing quotation mark.
|
|
|
|
Since the type of "c" is "I_p ...", the constructor should
return the value of it.
|
|
|
