| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Example: add this to the first block in
canonical-structures.rst:
~~~
Check nat.
Check nat nat.
~~~
Output:
~~~
reading sources... [ 2%] addendum/canonical-structures
Extension error:
/home/gaetan/dev/coq/coq/doc/sphinx/addendum/canonical-structures.rst:43: Error while sending the following to coqtop:
Check nat nat.
coqtop output:
Toplevel input, characters 6-13:
> Check nat nat.
> ^^^^^^^
[37;41;1mError:[0m Illegal application (Non-functional construction):
The expression "nat" of type "[33;1mSet[0m"
cannot be applied to the term
"nat" : "[33;1mSet[0m"
Full error text:
End Of File (EOF). Exception style platform.
<pexpect.pty_spawn.spawn object at 0x7fc8c8b1bc18>
command: /home/gaetan/dev/coq/coq/bin/coqtop
args: [b'/home/gaetan/dev/coq/coq/bin/coqtop', b'-boot', b'-color', b'on']
buffer (last 100 chars): ''
before (last 100 chars): 'xpression "nat" of type "\x1b[33;1mSet\x1b[0m"\r\ncannot be applied to the term\r\n "nat" : "\x1b[33;1mSet\x1b[0m"\r\n'
after: <class 'pexpect.exceptions.EOF'>
match: None
match_index: None
exitstatus: None
flag_eof: True
pid: 11150
child_fd: 5
closed: False
timeout: 30
delimiter: <class 'pexpect.exceptions.EOF'>
logfile: None
logfile_read: None
logfile_send: None
maxread: 2000
ignorecase: False
searchwindowsize: None
delaybeforesend: 0
delayafterclose: 0.1
delayafterterminate: 0.1
searcher: searcher_re:
0: re.compile('\r\n[^< ]+ < ')
make[1]: *** [Makefile.doc:65: refman-html] Error 2
~~~
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
|
|
This uses a new coqtop-only option "Coqtop Exit On Error", not sure where
to put the doc for it. It being an option means we can locally turn it
off (.. coqtop:: fail).
|
|
|
|
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Ack-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
|
|
We change regen_readme such that when given an argument it outputs
there instead of overwriting the readme.
Prompted by me noticing I forgot to regen in #9553.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Reviewed-by: cpitclaudel
|
|
It was used in the standard library and the test-suite but undocumented so far.
|
|
|
|
|
|
|
|
|
|
binders.
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: Zimmi48
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Mostly in the pattern
~~~
.. coqtop:: in
Theorem foo : bla.
Theorem bar : blah. (* nested proof error *)
~~~
|
|
|
|
|
|
In particular, mention that auto does not use full-blown apply.
|
|
|
|
Maybe we should still let it run but let's disable it until we install
csdp on the build server at least.
|
|
|
|
|
|
|
|
Not sure why but it seems required for future commits.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
In fixpoint typing rule section, a type of constructor is described
twice:
- ∀ p_1:P_1,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_r:T_r,~(I_j~p_1 … p_r~t_1 … t_s)
- ∀ p_1:P_1,~…,∀ p_r :P_r,~∀ y_1:B_1,~… ∀ y_k:B_k,~(I~a_1 … a_k)
Both seems invalid.
The former require that the number of parameters and
the number of (non-parameter) constructor argumets is same.
The latter require that the number of (non-parameter) constructor
argumets and the number of inductive type arguments (including paramters) is
same.
Also, "k" is already used for the number of inductive types in
a inductive definition.
So, I changed the number of (non-parameter) constructor
argumets to "m". I choose "m" because "m" is used for the purpose
in the description for iota-reduction of destructors.
Also, I changed the inductive type parameters and arguments of latter
consistent with the former.
|
|
In the description of destructors,
"Type of branches" section and "Typing rule" section shares
the definition of "r" (and "s" from previous commit).
However actual parameters are p_1...p_r in the former section and
q_1...q_r in the latter section.
I guess it's because the latter section uses
p_1...p_l in other purpose: index of constructor for a inductive type.
So, I change the parameter p_1...p_r to q_1...q_r in the former section
to consistent with the latter section.
|
