aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-01-31Remove "End TreeExample." line.Tanaka Akira
This corresponds to "Module TreeExample." removed at 2018-04-24 bcf5352cc7a26a672e719f7dad4021c69d723833.
2019-01-31Merge PR #8720: [Numeral notations] Use Coqlib registered constantsEmilio Jesus Gallego Arias
Reviewed-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: vbgl
2019-01-30Update Cachix signing key.Théo Zimmermann
2019-01-30Updated pinned nixpkgs.Théo Zimmermann
Use default OCaml version (4.06.1).
2019-01-30Merge PR #9440: Create deployment environment for Cachix.Emilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: ejgallego
2019-01-30Create deployment environment for Cachix.Théo Zimmermann
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments.
2019-01-30Cleanup universe length for inductives in vconvGaëtan Gilbert
2019-01-30Restrict universes in records.Gaëtan Gilbert
Fix #8076.
2019-01-30Comment universe operations in Classes.contextGaëtan Gilbert
2019-01-30Merge pull request coq/ltac2#100 from JasonGross/fix-lazy-match-goalPierre-Marie Pédrot
Make lazy_match! goal actually lazy
2019-01-29Merge PR #9417: Update update-compat.py scriptThéo Zimmermann
Reviewed-by: Zimmi48
2019-01-29Merge PR #9435: Use \mathcal instead of \calThéo Zimmermann
Reviewed-by: Zimmi48
2019-01-29Update update-compat.py scriptJason Gross
It now removes the outdated `CompatOldOldFlag.v` file on `--release`, and it now correctly updates `bug_9166.v` which seems to specifically be about the compat flag behavior. Additionally, it inserts an "autogenerated" notice at top of the two bug files, and makes them read-only.
2019-01-29Merge PR #9274: Make `Instance` without a body always open a proofEnrico Tassi
Reviewed-by: gares Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-01-29[test-suite] Display full paths on CHECK.Emilio Jesus Gallego Arias
This makes the display consistent wrt `TEST`: ``` TEST failure/Case7.v CHECK Case7 ``` vs ``` TEST failure/Case7.v CHECK failure/Case7.v ```
2019-01-29Use \mathcal instead of \calGaëtan Gilbert
Apparently it's deprecated / doesn't always work, see https://tex.stackexchange.com/questions/84041/why-does-calm-n-give-m See #9429 (we also need to fix the distributed file on the server).
2019-01-29Merge PR #9421: [vernac] Fix classification of `Declare Custom Entry`Enrico Tassi
Reviewed-by: gares
2019-01-29Merge PR #9383: Remove travisVincent Laporte
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2019-01-29Merge PR #9424: Surround "assumption" with :tacn:`` in tactics.rstThéo Zimmermann
Reviewed-by: jfehrle
2019-01-29[test-suite] Fix display of check.Emilio Jesus Gallego Arias
After #8655
2019-01-28Make lazy_match! goal actually lazyJason Gross
It was missing `Control.once`. Fixes coq/ltac2#79 Fixes coq/ltac2#77
2019-01-28Surround "assumption" with :tacn:`` in tactics.rstRyan Scott
2019-01-28Merge PR #9420: [doc] Remove emacs mentions from INSTALLThéo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2019-01-28[vernac] Fix classification of `Declare Custom Entry`Emilio Jesus Gallego Arias
It seems that this command should be classified as modifying the parser. Fixes #9419 Thanks to @gares
2019-01-28[doc] Remove emacs mentions from INSTALLEmilio Jesus Gallego Arias
Fixes #9418
2019-01-28Merge pull request coq/ltac2#94 from maximedenes/proof-modePierre-Marie Pédrot
Adapt to Coq's new proof mode API
2019-01-28Merge PR #9402: Move \def\plus and \def\tri to refman-preamble.sty.Théo Zimmermann
Reviewed-by: Zimmi48
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
Reviewed-by: CohenCyril Ack-by: Zimmi48 Ack-by: gares Reviewed-by: maximedenes
2019-01-27Merge PR #9399: [ide] fail on unavailable commands before adding to the documentEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: ppedrot
2019-01-27[test] for bug #9385Enrico Tassi
2019-01-27[fake_ide] infrastructure to test the failure of an ADDEnrico Tassi
2019-01-27[ide] fail on unavailable commands before adding to the documentEnrico Tassi
2019-01-27Merge PR #9263: [STM] explicit handling of parsing statesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares Ack-by: maximedenes
2019-01-27Merge PR #9214: Notations: Removing useless parentheses on abbreviations ↵Emilio Jesus Gallego Arias
shortening a strict prefix of an application Reviewed-by: ejgallego
2019-01-26Simplify the GitHub issue templateTej Chajed
2019-01-25Move non-primitive-record warning to declare_mutual_inductive_with_eliminationsGaëtan Gilbert
This makes it print the warning before the definition message, so if we run with +non-primitive-record we don't see """ defined foo error could not define foo """
2019-01-25Merge PR #9362: Fix makefile .merlin for unit testsEnrico Tassi
Reviewed-by: gares
2019-01-25Merge PR #9391: Clarify meaning of Primitive ProjectionsThéo Zimmermann
Reviewed-by: Zimmi48
2019-01-25Merge PR #8637: Update -compat to support -compat 8.10Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares
2019-01-25Added a line about notation bug fixes.Hugo Herbelin
2019-01-25Notations: Removing useless parentheses on abbrevs for prefix of an application.Hugo Herbelin
2019-01-25[Numeral notations] Lazy resolution of decimal typesVincent Laporte
2019-01-25[Numeral notations] Use Coqlib registered constantsVincent Laporte
2019-01-24Merge PR #9325: Stop [Print] from saying [is (not) universe polymorphic].Hugo Herbelin
Reviewed-by: maximedenes
2019-01-24Add some quot/rem test-cases for niaJason Gross
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, ↵Jason Gross
Z.to_euclidean_division_equations
2019-01-24Update CHANGESJason Gross
2019-01-24Revert "Add subst to the end of nia in the test-suite"Jason Gross
This reverts commit b49f4e966443a76ac70d37c4cde68f94de164c01. It turns out the 4x was due to .nia.cache (because I didn't clean sufficiently in testing), not due to `subst`.
2019-01-24Add subst to the end of nia in the test-suiteJason Gross
This speeds up the file from 2m32s to ``` real 0m41.851s user 0m41.512s sys 0m0.376s ``` Also note the `subst` trick in the doc.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-25 22:28:12 +0000