aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-08-17Merge PR #490: A possible fix for #5391 (command line tools do not accept ↵Maxime Dénès
trailing / and \ on windows)
2017-08-17Merge PR #974: Change section caption, improve some wordingMaxime Dénès
2017-08-17Merge PR #976: Document anonymous universes (PR #544).Maxime Dénès
2017-08-17Document anonymous universes (PR #544).Gaëtan Gilbert
2017-08-16mention that tactic is the identity or gives errorPaul Steckler
2017-08-16change section caption, improve some wordingPaul Steckler
2017-08-16Merge PR #957: Set detachable windows type hint to dialog.Maxime Dénès
2017-08-16Merge PR #831: Port ssreflect user manual to Coq's latex/hevea styleMaxime Dénès
2017-08-16Merge PR #912: Detyping functions are now operating on EConstr.t.Maxime Dénès
2017-08-16Merge PR #942: solving b1859Maxime Dénès
2017-08-16Merge PR #954: Print names of all open blocksMaxime Dénès
2017-08-16Merge PR #964: More portable location for the time command.Maxime Dénès
2017-08-16Merge PR #951: Makefile: install-byte works even if -coqide noMaxime Dénès
2017-08-16Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsMaxime Dénès
2017-08-16Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)Maxime Dénès
2017-08-16Merge PR #944: Fix typos. Improve wording.Maxime Dénès
2017-08-16Merge PR #943: Reference Manual: minor wording improvementsMaxime Dénès
2017-08-16Merge PR #940: Replace jarring use of "Remark" with "Note"Maxime Dénès
2017-08-16Merge PR #934: Fix some coq-tex errors in the reference manual.Maxime Dénès
2017-08-16Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵Maxime Dénès
wrongly tagged as keywords
2017-08-16Merge PR #864: Some cleanups after cumulativity for inductive typesMaxime Dénès
2017-08-15Removing trailing "/" and "\" in directory names only on win32.Hugo Herbelin
This refines e234f3ef. By the way, note that e234f3ef fixed #5391 (command line tools do not accept trailing "/" - or "\" - in windows).
2017-08-15Adding a test for BZ#1859 as suggested by @tchajed.Théo Zimmermann
2017-08-12Merge PR #963: fix coq_makefileMaxime Dénès
2017-08-12fix coq_makefileMatej Košík
Make sure that when plugin writer does not use -bypass-API, API is opened by default.
2017-08-12More portable location for the time command.Théo Zimmermann
On NixOS in particular, /usr/bin/time doesn't exist.
2017-08-08Set detachable windows type hint to dialog.Olivier Marty
Windows such as Search & Replace are dialogs. For some window managers, the hint changes how the window is displayed.
2017-08-06Print names of all open blocksTej Chajed
Fixes bug 5597.
2017-08-04Makefile: install-byte works even if -coqide noEnrico Tassi
2017-08-03Amend wording to capture intended meaningSam Pablo Kuper
per @Zimmi48's comments [here](https://github.com/coq/coq/pull/944#discussion_r131072333) and [here](https://github.com/coq/coq/pull/944#discussion_r131072790).
2017-08-02Rewording the introductionEnrico Tassi
The contents should be exactly the same. I removed the distinction between tactical and pseudo-tactical because I think that it is too much technical for the introduction. I used "syntactic construction" and made appeal to the reader intuition by saying that such construction behaves similarly to a tactical. I think the text would be much more readable if "the tactics described in Chapter..." could be replaced by a *name*, but I'm afraid the only one I could use (Ltac) is a bit too ambiguous. So I'm open to suggestions.
2017-08-02Rephrasing a couple of sentences in a more factual way.Hugo Herbelin
2017-08-02Rephrasing the introduction in a more factual and up-to-date way.Hugo Herbelin
2017-08-02Port ssr manual to Coq's latex/hevea styleEnrico Tassi
Work done by Assia Mahboubi and Enrico Tassi
2017-08-02Makefile.doc: implement serve-refman-8080 targetEnrico Tassi
We make it so that, by default, the HTML reference manual looks like the one published online (same .css) and we provide a target to serve it locally (requires python).
2017-08-02Update Setoid.texlarsr
The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`.
2017-08-02Makefile: 'make clean' now immune to the check for binary files without sourcesPierre Letouzey
This is a followup of 7d1fc15. Without this fix, you're warned of leftover files, but even a 'make clean' is then refused, so you cannot get rid of them easily (apart via a git clean -xfd).
2017-08-02Typo in the documentation of cumulativityAmin Timany
2017-08-01Printing goals does not evar-normalizes beforehand anymore.Pierre-Marie Pédrot
2017-08-01Detyping functions are now operating on EConstr.t.Pierre-Marie Pédrot
This was already the case, but the API was not exposing this.
2017-08-01Fix typos. Improve wording.Sam Pablo Kuper
2017-08-01Improve style slightlySam Pablo Kuper
per @aspiwack's comments in [this pull request review](https://github.com/coq/coq/pull/940).
2017-08-01Merge PR #933: Fix documentation of Hint Mode (bug #4911).Maxime Dénès
2017-08-01Merge PR #932: Fix shuffled documentation.Maxime Dénès
2017-08-01Merge PR #929: Add missing paragraph to introductionMaxime Dénès
2017-08-01Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Maxime Dénès
2017-08-01Merge PR #926: test-suite uses Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #925: Document Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #921: [make] remove compat5 file.Maxime Dénès
2017-08-01Merge PR #919: Remove a few useless evar-normalizations in printing code.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 09:23:14 +0000