| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-17 | Merge PR #861: Fix typo in documentation for identity | Maxime Dénès | |
| 2017-07-13 | Set version to 8.7+alpha. | Maxime Dénès | |
| It is a valid git tag (unlike 8.7~alpha) and will be considered by most tools as < 8.7.0 (unlike 8.7.0+alpha). | |||
| 2017-07-11 | Merge PR #858: [travis] Remove CompCert version check hack. | Maxime Dénès | |
| 2017-07-11 | Merge PR #860: use Int.equal instead of polymorphic = | Maxime Dénès | |
| 2017-07-07 | Merge PR #863: Fixing environment in warning "Projection value has no head ↵ | Maxime Dénès | |
| constant". | |||
| 2017-07-07 | Merge PR #842: Update the Tutorial. | Maxime Dénès | |
| 2017-07-07 | Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ↵ | Maxime Dénès | |
| the monad. | |||
| 2017-07-07 | Merge PR #835: Remove doc/refman/RefMan-ind.tex | Maxime Dénès | |
| 2017-07-07 | Set version to 8.7.0~alpha. | Maxime Dénès | |
| 2017-07-07 | Merge PR #844: Better support for make TIMED=1 on Windows | Maxime Dénès | |
| 2017-07-07 | Merge PR #800: Enable fiat-crypto | Maxime Dénès | |
| 2017-07-07 | Fixing environment in warning "Projection value has no head constant". | Hugo Herbelin | |
| Delaying also some computation needed for printing to the time of really printing it. | |||
| 2017-07-05 | Fix typo in documentation for identity | Tej Chajed | |
| Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635). | |||
| 2017-07-05 | use Int.equal instead of polymorphic = | Paul Steckler | |
| 2017-07-05 | [travis] Remove CompCert version check hack. | Emilio Jesus Gallego Arias | |
| We now pass `-ignore-coq-version` to CompCert's configure (cf AbsInt/CompCert#188) , thanks to @xavierleroy . | |||
| 2017-07-05 | Merge PR #837: Add inversion_sigma to CHANGES and to doc | Maxime Dénès | |
| 2017-07-05 | Merge PR #850: Improve grammar in RefMan-Gal and RefMan-syn | Maxime Dénès | |
| 2017-07-05 | Merge PR #840: Quote $(OCAMLFIND) in CoqMakefile.in for Windows | Maxime Dénès | |
| 2017-07-05 | Merge PR #839: Update .gitignore with doc/tutorial/Tutorial.v.out | Maxime Dénès | |
| 2017-07-05 | Merge PR #832: Document an example `Makefile` for `coq_makefile` | Maxime Dénès | |
| 2017-07-04 | Revert fiat-crypto overlay | Jason Gross | |
| Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6. | |||
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-07-01 | Update RefMan-syn.tex | william-lawvere | |
| 2017-07-01 | Merge remote-tracking branch 'upstream/trunk' into trunk | William Lawvere | |
| 2017-07-01 | RefMan-gal: improve grammar | William Lawvere | |
| 2017-07-01 | RefMan-syn: grammar edit | William Lawvere | |
| 2017-06-30 | Document an example `Makefile` for `coq_makefile` | Jason Gross | |
| We document an example `Makefile` which does not include the generated `CoqMakefile`, but instead invokes arbitrary targets in it. | |||
| 2017-06-30 | Remove doc/refman/RefMan-ind.tex | Jason Gross | |
| It does not seem to be referred to by any file, and does not seem to be built by any implicit rules. | |||
| 2017-06-30 | Add doc for inversion_sigma to RefMan-tac | Jason Gross | |
| 2017-06-30 | Update CHANGES with inversion_sigma entry | Jason Gross | |
| 2017-06-30 | Update .gitignore with doc/tutorial/Tutorial.v.out | Jason Gross | |
| 2017-06-30 | Fix more potential quoting issues: COQBIN , COQLIB | Jason Gross | |
| 2017-06-30 | Also quote $(COQLIB)/grammar | Jason Gross | |
| In case COQLIB has backslashes, as it does on Windows, or spaces | |||
| 2017-06-30 | Create a variable for CAMLDOC in CoqMakefile.in | Jason Gross | |
| 2017-06-30 | Quote $(OCAMLFIND) in CoqMakefile.in for Windows | Jason Gross | |
| This, I hope, will fix [bug #5620](https://coq.inria.fr/bugs/show_bug.cgi?id=5620) | |||
| 2017-06-30 | Better support for make TIMED=1 on Windows | Jason Gross | |
| This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619) | |||
| 2017-06-30 | Merge PR#846: Fix OS X Travis by pinning OCaml version. | Maxime Dénès | |
| 2017-06-30 | Merge PR#843: closing bug #5618 introduce by PR 828 | Maxime Dénès | |
| 2017-06-30 | Mention again how to report bug and get version number. | Théo Zimmermann | |
| As suggested by @psteckler. | |||
| 2017-06-30 | Fix OS X Travis by pinning OCaml version. | Théo Zimmermann | |
| 2017-06-29 | Better phrasing. | Théo Zimmermann | |
| 2017-06-29 | More substance on discouraged practices. | Théo Zimmermann | |
| 2017-06-29 | closing bug #5618 introduce by PR 828 | Julien Forest | |
| 2017-06-29 | Some more corrections to the tutorial. | Théo Zimmermann | |
| 2017-06-29 | Mask the reliance on coqtop. | Théo Zimmermann | |
| 2017-06-28 | Update the Tutorial. | Théo Zimmermann | |
| 2017-06-27 | Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵ | Maxime Dénès | |
| with make -j4 | |||
| 2017-06-27 | Merge PR#731: Mini-cleaning around OCaml file names | Maxime Dénès | |
| This is only a partial merge, we stick with using the standard OCaml (un)capitalize functions. | |||
| 2017-06-27 | A cleaning phase about ocaml file names. | Hugo Herbelin | |
| Ocaml file names are restricted since 2008 to A..Z followed by a..z0..9'_. We take this constraint into account in tools manipulating Ocaml file names. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |