aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-19[sphinx] Refactor handling of options for coqtop directive.Théo Zimmermann
Make it mandatory to give exactly one display option.
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 #9589: Deprecate duplicated explicitation_eqEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin Ack-by: jashug
2019-02-18Merge PR #9600: CI: fix trunk jobs switch pickingEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-18Merge PR #9597: [ci] Resolve commit corresponding to branch when downloading ↵Emilio Jesus Gallego Arias
tarball. Reviewed-by: SkySkimmer Reviewed-by: ejgallego
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2019-02-18Merge PR #9592: Fix per-commit linting with bot mergesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-18Merge PR #9599: Remove undefined install_printer ppcumulativity_infoEmilio Jesus Gallego Arias
2019-02-18CI: fix trunk jobs switch pickingGaëtan Gilbert
After #9590 Instead of this we could override before_script, either duplicating the debug prints or just not doing debug prints for the trunk jobs.
2019-02-18Remove undefined install_printer ppcumulativity_infoGaëtan Gilbert
2019-02-18[ci] Resolve commit corresponding to branch when downloading tarball.Théo Zimmermann
This ensures that the log will contain the commit hash that we tested. This reuses the method from the Windows build script (we have a number of common functions, it would be interesting to start a bash shared library file).
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-18Merge PR #9590: [gitlab] [docker] [ci] Remove "edge" compiler switch.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-18Fix per-commit linting with bot mergesGaëtan Gilbert
When the bot auto-merged the linter saw no commits to lint, eg https://gitlab.com/coq/coq/-/jobs/162893603 I'm pushing from a non-current master so we will see if this works.
2019-02-18Merge PR #9439: Separate variance and universe fields in inductives.Pierre-Marie Pédrot
Ack-by: ppedrot
2019-02-18Merge PR #9509: Fix #9508: Unexpected interaction between implicit arguments ↵Maxime Dénès
and primititive projections Reviewed-by: maximedenes
2019-02-18[gitlab] [docker] [ci] Remove "edge" compiler switch.Emilio Jesus Gallego Arias
Since a long time the compiler switch is not very useful as it is not used to test any CI. The `edge+flambda` version seems stable enough to carry out the `edge` testing by itself, thus we remove the `egde` switch saving valuable Docker image size and Gitlab runners. We also tweak the `pkg:opam` job as to correctly set the version of the pinned local package.
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
I think the usage looks cleaner this way.
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-17Merge PR #9549: [ide] fix unconditional goto-point on editing an error (fix ↵Pierre-Marie Pédrot
#9488) Ack-by: gares Ack-by: maximedenes Reviewed-by: ppedrot
2019-02-17Merge PR #9506: Remove some non tailrec List.map from CList implementationsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-02-16Deprecated duplicated explicitation_eqJasper Hugunin
2019-02-14Merge PR #9571: Document the now_show tactic.Clément Pit-Claudel
Ack-by: Zimmi48 Reviewed-by: cpitclaudel
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-14Merge PR #9502: Remove nondeterministic testsThéo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2019-02-14Merge PR #9542: [Manual] Don’t use `Undo`; and other cleaningThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: maximedenes
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 #9554: Don't save expected failure logs from opened/ bugs.Maxime Dénès
Reviewed-by: maximedenes
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-13more testsEnrico Tassi
2019-02-13refactor grammarEnrico Tassi
2019-02-13Fix #9432: canonical structure and coercion accept universe binders.Gaëtan Gilbert
(when defining a new constant)
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-13Merge PR #9557: [ssreflect] Export more parsing witnesses.Enrico Tassi
2019-02-13Merge PR #9173: [tactics] Remove dependency of abstract on global proof state.Maxime Dénès
Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: mattam82 Ack-by: maximedenes Reviewed-by: ppedrot
2019-02-12Merge PR #9548: Almost fully type-safe gramlib implementationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 13:53:07 +0000