aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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 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-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-24Merge PR #9325: Stop [Print] from saying [is (not) universe polymorphic].Hugo Herbelin
Reviewed-by: maximedenes
2019-01-24Update update-compat.py and release-process.mdJason Gross
In response to review comments by Zimmi48
2019-01-24Update -compat to support -compat 8.10Jason Gross
This commit was created via `./dev/tools/update-compat.py --master`
2019-01-24Update update-compat.py scriptJason Gross
We now support --master and --release. On the master branch, we support four compatibility versions, while on releases and release branches, we support only three compatibility versions. We also support --git-add to automatically run `git add` with new and updated files, and to run `git rm` with deleted files.
2019-01-25Move \def\plus and \def\tri to refman-preamble.sty.Tanaka Akira
The definition of \plus and \tri in cic.rst is not effective for HTML output. So, move them into refman-preamble.sty. Also, \tri is renamed to \trii to express the suffix of "\triangleright_\iota".
2019-01-24Merge PR #9384: Improve the note in the beginning of the Ltac chapter.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-01-24Add OverlaysMaxime Dénès
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
DAG nodes hold now a system state and a parsing state. The latter is always passed to the parser. This paves the way to decoupling the effect of commands on the parsing state and the system state, and hence never force to interpret, say, Notation. Handling proof modes is now done explicitly in the STM, not by interpreting VernacStartLemma. Similarly Notation execution could be split in two phases in order to obtain a parsing state without fully executing it (that requires executing all commands before it). Co-authored-by: Maxime Dénès <maxime.denes@inria.fr> Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
2019-01-24[STM] API to print a Stateid.tEnrico Tassi
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-24Merge PR #9269: Move and rewrite intro pattern sectionThéo Zimmermann
Ack-by: Zimmi48 Ack-by: anton-trunov Ack-by: jfehrle
2019-01-24Merge PR #9392: Fix small errors in cic.rst.Théo Zimmermann
Reviewed-by: Zimmi48
2019-01-24Merge PR #9394: [nix-ci] MaintenanceThéo Zimmermann
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: maximedenes
2019-01-24[nix-CI] Split the build inputsVincent Laporte
Coq and the Coq libraries can now be excluded (by setting the NOCOQ environment variable).
2019-01-24[Nix-ci] Add QuickChickVincent Laporte
2019-01-24[Nix-ci] Fix UnicoqVincent Laporte
2019-01-24[Nix-ci] Add formal-topologyVincent Laporte
2019-01-24Merge PR #9377: [CS] recognize applied primitive projections as keys (fix #9375)Matthieu Sozeau
Ack-by: SkySkimmer Ack-by: gares Reviewed-by: mattam82 Ack-by: ppedrot
2019-01-24[doc] warn that (automatic) clears can result in errorsEnrico Tassi
2019-01-24[doc] more precise description of when automatic clears are triggeredEnrico Tassi
2019-01-24[doc] explain how to avoid automatic clearsEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:06:47 +0000