aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-18[sphinx] Add abort and restart options to directive coqtop.Théo Zimmermann
2019-02-18coqdomain.py fix typo in commentGaëtan Gilbert
2019-02-18Sphinx: nicer error reportingGaëtan Gilbert
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. > ^^^^^^^ Error: Illegal application (Non-functional construction): The expression "nat" of type "Set" cannot be applied to the term "nat" : "Set" 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>
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
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).
2019-02-18Fix doc for Refine Instance ModeGaëtan Gilbert
2019-02-18Sphinx: remove [coqtop:: undo]Gaëtan Gilbert
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2019-02-18Fix last nested lemma failure.Théo Zimmermann
2019-02-18Fix failing coqtops in type-classes.rstGaëtan Gilbert
2019-02-18Merge PR #9568: Add test that we regenerated doc/sphinx/README.rst to linterThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2019-02-18Add diff rule for README.rst to dune refman-html aliasGaëtan Gilbert
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.
2019-02-17Merge PR #9528: Fix #9527: unknown evar in nonterminating [fix] error.Pierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-02-14Merge PR #9571: Document the now_show tactic.Clément Pit-Claudel
Ack-by: Zimmi48 Reviewed-by: cpitclaudel
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
Instead, if the coqlib is special, we set it explicitly in the command line, as Dune does. This is a continuation of #9523. In Sphinx, we stop using -boot, and pass `-coqlib` through the environment instead. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2019-02-14Document the now_show tactic.Théo Zimmermann
It was used in the standard library and the test-suite but undocumented so far.
2019-02-14[Manual] Fix a referenceVincent Laporte
2019-02-14[Manual] Clean examples for `apply`Vincent Laporte
2019-02-14[Manual] Don’t use `Undo` in ssreflect examplesVincent Laporte
2019-02-14[Manual] Clean examples about `inversion` tacticVincent Laporte
2019-02-13Merge PR #9450: Fix #9432: canonical structure and coercion accept universe ↵Maxime Dénès
binders. Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares Reviewed-by: maximedenes
2019-02-13[ssr] move shorter Canonical to Coq properEnrico Tassi
2019-02-13Merge PR #9564: Fix small errors in cic.rst (3rd)Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-13Merge PR #9553: Sphinx various fixing of failing commandsThéo Zimmermann
Ack-by: Zimmi48
2019-02-12Fix failing coqtops in syntax-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in tactics.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ssreflect-proof-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ltac.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coqide.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-specification-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coq-library.rstGaëtan Gilbert
Mostly in the pattern ~~~ .. coqtop:: in Theorem foo : bla. Theorem bar : blah. (* nested proof error *) ~~~
2019-02-12Fix failing coqtops in cic.rstGaëtan Gilbert
2019-02-12Fix failing coqtops universe-polymorphism.rstGaëtan Gilbert
2019-02-12Improve the documentation of auto.Théo Zimmermann
In particular, mention that auto does not use full-blown apply.
2019-02-12Fix failing coqtops in ring.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in micromega.rst (the main one requires csdp)Gaëtan Gilbert
Maybe we should still let it run but let's disable it until we install csdp on the build server at least.
2019-02-12Fix failing coqtops in generalized-rewriting.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in extended-pattern-matching.rstGaëtan Gilbert
2019-02-12Fix doc for coqtop:: undoGaëtan Gilbert
2019-02-12Increase sphinx recursion limitGaëtan Gilbert
Not sure why but it seems required for future commits.
2019-02-11Small typos in the documentation.Martin Bodin
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-11Use math mode more.Tanaka Akira
Also quoted parts are emphasized as coq-8.7.2-reference-manual.pdf. And two "x:T" are quoted.
2019-02-11Use {LEFT,RIGHT} DOUBLE QUOTATION MARK.Tanaka Akira
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.
2019-02-11Remove a space before closing double-quote.Tanaka Akira
2019-02-10Change "I" to "I_p".Tanaka Akira
Since the type of "c" is "I_p ...", the constructor should return the value of it.
2019-02-10Distinguish inductive {definition,inductive}.Tanaka Akira
2019-02-09Update link to refman and stdlib doc for master branch.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 19:28:40 +0000