| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-18 | Merge PR #973: Adding documentation for Printing Focused option. | Maxime Dénès | |
| 2017-08-18 | Merge PR #801: Make Travis generate OSX packages. | Maxime Dénès | |
| 2017-08-18 | Separate jobs for test-suite and package building under OSX. | Maxime Dénès | |
| 2017-08-17 | Merge PR #972: 8.7 change entries | Maxime Dénès | |
| 2017-08-17 | Merge PR #490: A possible fix for #5391 (command line tools do not accept ↵ | Maxime Dénès | |
| trailing / and \ on windows) | |||
| 2017-08-17 | Merge PR #974: Change section caption, improve some wording | Maxime Dénès | |
| 2017-08-17 | Merge PR #976: Document anonymous universes (PR #544). | Maxime Dénès | |
| 2017-08-17 | Use the wording suggested by Gaetan. | Théo Zimmermann | |
| 2017-08-17 | Addition suggested by Pierre-Marie. | Théo Zimmermann | |
| 2017-08-17 | Change 8.7~alpha to 8.7+alpha. | Maxime Dénès | |
| Only the latter is a valid git tag, and we will soon be using those to generate our version numbers. | |||
| 2017-08-17 | Make Travis generate OSX packages. | Maxime Dénès | |
| The packages will be built only for main branches (not pull requests), and are accessible via bintray: https://bintray.com/coq/coq | |||
| 2017-08-17 | Document anonymous universes (PR #544). | Gaëtan Gilbert | |
| 2017-08-17 | Adding documentation for Printing Focused option. | Pierre Courtieu | |
| 2017-08-16 | Additions following Hugo's suggestions. | Théo Zimmermann | |
| 2017-08-16 | mention that tactic is the identity or gives error | Paul Steckler | |
| 2017-08-16 | Improve wording. | Théo Zimmermann | |
| 2017-08-16 | Mention tclINDEPENDENTL (#349) in dev/doc/changes. | Théo Zimmermann | |
| 2017-08-16 | 8.7 CHANGES | Théo Zimmermann | |
| 2017-08-16 | change section caption, improve some wording | Paul Steckler | |
| 2017-08-16 | Porting #856 (8.6.1 CHANGES entries) to master | Théo Zimmermann | |
| 2017-08-16 | Merge PR #957: Set detachable windows type hint to dialog. | Maxime Dénès | |
| 2017-08-16 | Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style | Maxime Dénès | |
| 2017-08-16 | Merge PR #912: Detyping functions are now operating on EConstr.t. | Maxime Dénès | |
| 2017-08-16 | Merge PR #942: solving b1859 | Maxime Dénès | |
| 2017-08-16 | Merge PR #954: Print names of all open blocks | Maxime Dénès | |
| 2017-08-16 | Merge PR #964: More portable location for the time command. | Maxime Dénès | |
| 2017-08-16 | Merge PR #951: Makefile: install-byte works even if -coqide no | Maxime Dénès | |
| 2017-08-16 | Merge PR #841: Timorous fix of bug #5598 on global existing class in sections | Maxime Dénès | |
| 2017-08-16 | Merge PR #948: [doc] Write (@nil nat) instead of (nil nat) | Maxime Dénès | |
| 2017-08-16 | Merge PR #944: Fix typos. Improve wording. | Maxime Dénès | |
| 2017-08-16 | Merge PR #943: Reference Manual: minor wording improvements | Maxime Dénès | |
| 2017-08-16 | Merge PR #940: Replace jarring use of "Remark" with "Note" | Maxime Dénès | |
| 2017-08-16 | Merge PR #934: Fix some coq-tex errors in the reference manual. | Maxime Dénès | |
| 2017-08-16 | Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵ | Maxime Dénès | |
| wrongly tagged as keywords | |||
| 2017-08-16 | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 2017-08-15 | Removing 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-15 | Adding a test for BZ#1859 as suggested by @tchajed. | Théo Zimmermann | |
| 2017-08-12 | Merge PR #963: fix coq_makefile | Maxime Dénès | |
| 2017-08-12 | fix coq_makefile | Matej Košík | |
| Make sure that when plugin writer does not use -bypass-API, API is opened by default. | |||
| 2017-08-12 | More portable location for the time command. | Théo Zimmermann | |
| On NixOS in particular, /usr/bin/time doesn't exist. | |||
| 2017-08-08 | Set 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-06 | Print names of all open blocks | Tej Chajed | |
| Fixes bug 5597. | |||
| 2017-08-04 | Makefile: install-byte works even if -coqide no | Enrico Tassi | |
| 2017-08-03 | Amend wording to capture intended meaning | Sam 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-02 | Rewording the introduction | Enrico 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-02 | Rephrasing a couple of sentences in a more factual way. | Hugo Herbelin | |
| 2017-08-02 | Rephrasing the introduction in a more factual and up-to-date way. | Hugo Herbelin | |
| 2017-08-02 | Port ssr manual to Coq's latex/hevea style | Enrico Tassi | |
| Work done by Assia Mahboubi and Enrico Tassi | |||
| 2017-08-02 | Makefile.doc: implement serve-refman-8080 target | Enrico 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-02 | Update Setoid.tex | larsr | |
| The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |