| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-19 | Rename coq-inferior.el -> inferior-coq.el to match provided feature. | Gaëtan Gilbert | |
| Fixes #4988. | |||
| 2017-11-13 | coq_makefile: document COQ_SRC_SUBDIRS | Enrico Tassi | |
| 2017-11-06 | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]", | Samuel Gruetter | |
| not "first [ progress tac1 | progress tac2 ]". And add a missing backslash. | |||
| 2017-11-06 | Merge PR #1139: Add a linter. | Maxime Dénès | |
| 2017-10-27 | Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631 | Maxime Dénès | |
| 2017-10-25 | Rename \Tree to \NatTree | Johannes Kloos | |
| 2017-10-25 | Put newlines at the end of files. | Gaëtan Gilbert | |
| 2017-10-24 | Fix #5763: Strictly positive example is out of order. | jkloos | |
| I also renamed the type to nattree (see discussion on https://github.com/coq/coq/pull/5979) to disambiguate from another, earlier example. | |||
| 2017-10-24 | Fix #4846 | Johannes Kloos | |
| Bug description: The "now" tactic, which is being used in the standard library, is not documented in the Reference Manual This commit documents the easy tactic, and gives now as a variant. | |||
| 2017-10-24 | Fix #5413: [unfold ... in] not documented | Johannes Kloos | |
| Made a description of unfold...in and moved the index entry there. | |||
| 2017-10-24 | Documentation: Add various basic constructs to the index. | Johannes Kloos | |
| This was mentioned in #5631 as well. Now, forall, fun and casts have index entries. | |||
| 2017-10-24 | Fix part of 'Hard to find documentation for `(...) and `{...} #5631' | Johannes Kloos | |
| As discussed in the bug report, this adds `(...) and `{...} to the index. | |||
| 2017-10-11 | Remove GeoProof support. | Maxime Dénès | |
| Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq). | |||
| 2017-10-05 | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵ | Maxime Dénès | |
| to escape non-UTF-8 file names) | |||
| 2017-10-03 | Merge PR #1080: Remove some unused parts of the reference manual. | Maxime Dénès | |
| 2017-09-29 | [vernac] Remove `Qed exporting` syntax. | Emilio Jesus Gallego Arias | |
| We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why. | |||
| 2017-09-22 | Remove some unused parts of the reference manual. | Guillaume Melquiond | |
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond | |
| 2017-09-13 | Reference manual: A few words about the file system constraints for -Q/-R. | Hugo Herbelin | |
| 2017-09-11 | Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit` | Maxime Dénès | |
| 2017-09-11 | Merge PR #1035: Fix the introduction of SSR refman chapter. | Maxime Dénès | |
| 2017-09-11 | Merge PR #1014: Add option index entry for NativeCompute Profiling | Maxime Dénès | |
| 2017-09-11 | Merge PR #1004: Document primitive projections in more detail | Maxime Dénès | |
| 2017-09-08 | Fix Typo in Doc for `Set Parsing Explicit` | staffehn | |
| 2017-09-08 | Fix the introduction of SSR refman chapter. | Théo Zimmermann | |
| 2017-09-03 | 2 Typos in 'Add Parametric Morphism' Documentation | staffehn | |
| 2017-09-01 | add option index entry for NativeCompute Profiling | Paul Steckler | |
| 2017-08-31 | Document primitive projections in more detail | Matthieu Sozeau | |
| 2017-08-31 | RefMan-ssr: fix warning | Matthieu Sozeau | |
| 2017-08-31 | Merge PR #993: Credits for version 8.7 | Maxime Dénès | |
| 2017-08-31 | Credits for version 8.7 | Matthieu Sozeau | |
| 2017-08-31 | Merge PR #958: coq_makefile: build/use .cma for packed plugins too | Maxime Dénès | |
| 2017-08-29 | coq_makefile: improve documentation | Enrico Tassi | |
| 2017-08-29 | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | Maxime Dénès | |
| 2017-08-22 | Fix obsolete description of real numerals. | Guillaume Melquiond | |
| 2017-08-18 | use OCaml temp_file, instead of our own version | Paul Steckler | |
| 2017-08-18 | Merge PR #973: Adding documentation for Printing Focused option. | Maxime Dénès | |
| 2017-08-17 | Add native compute profiling, BZ#5170 | Paul Steckler | |
| 2017-08-17 | Merge PR #974: Change section caption, improve some wording | Maxime Dénès | |
| 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 | mention that tactic is the identity or gives error | Paul Steckler | |
| 2017-08-16 | change section caption, improve some wording | Paul Steckler | |
| 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 #948: [doc] Write (@nil nat) instead of (nil nat) | Maxime Dénès | |
| 2017-08-16 | Merge PR #943: Reference Manual: minor wording improvements | 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 #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |