aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-01-31Use \length for the function name of length.Tanaka Akira
2019-01-31Adjust spaces.Tanaka Akira
This commit basically ajusts spaces as - ∀x:T,t to ∀x:T,~t - λx:T.t to λx:T.~t - E;c:T to E;~c:T x and T are more related than T and t. So, T and t should not positioned closely than x and T. Unfortunately, they are formatted that T and t are positioned closely without "~". (Similary, c and T are more related than E and c.)
2019-01-31Use "∀" and "λ" instead of \forall and \lambda.Tanaka Akira
The former is more succinct and consistent with most of other parts in cic.rst.
2019-01-31Use math more.Tanaka Akira
Add :math:`...` for mathematical expressions.
2019-01-31Make parenthesis correctly matched.Tanaka Akira
2019-01-31\Sort is not a term.Tanaka Akira
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort" is changed to "∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S" because \Sort is not a term. "S" is choosen to be consistent with the description of Inductive Definitions.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:48:44 +0000