aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-01-31Use semicolon for separator of local contexts.Tanaka Akira
2019-01-31Don't line break at hyphen of compound words.Tanaka Akira
2019-01-31Move out a period and comma from :math:.Tanaka Akira
2019-01-31Nest :math: and parenthesis properly.Tanaka Akira
Exchange a closing parenthesis and a :math: closing backquote.
2019-01-31Fix syntax of two lambda-abstractions.Tanaka Akira
In the note about η-reduction, two lambda-abstraction used "," instead of ".".
2019-01-31Change {\Sort} to \Sort.Tanaka Akira
After #9435 (Use \mathcal instead of \cal), \Sort doesn't have font changing effect. So, {\Sort} is same as \Sort now and the former is changed to latter in cic.rst.
2019-01-31Use \Prop, \Set and \Type defined in refman-preamble.sty.Tanaka Akira
2019-01-31Make "1" and "2" in "f1" and "f2" suffixes.Tanaka Akira
2019-01-31Make "1" and "n" in "u1" and "un" suffixes.Tanaka Akira
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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:30:01 +0000