| Commit message (Collapse) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | | | | | | Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212 |  Maxime Dénès | 2017-12-05 | |
| |\ \ \ \ \ \ \ | |_|_|_|_|/ / |/| | | | | | | ||||
| | | * | | | | | clarify operation of sequences, #6095 |  Paul Steckler | 2017-12-01 | |
| | | | | | | | | ||||
| | | | * | | | | [refman] Expand a little on global universes. |  Matthieu Sozeau | 2017-12-01 | |
| | |_|/ / / / |/| | | | | | ||||
| | | | * | | | Documenting the -Q flag of coqchk. |  Pierre-Marie Pédrot | 2017-12-01 | |
| | | | | | | | ||||
| * | | | | | | Merge PR #6276: Coqchk accepts filenames | Maxime Dénès | 2017-12-01 | |
| |\ \ \ \ \ \ | |_|/ / / / |/| | / / / | | |/ / / | |/| | | | ||||
| | * | | | | Documenting the possibility to pass filenames to coqchk. | Pierre-Marie Pédrot | 2017-11-29 | |
| | | |/ / | |/| | | ||||
| | | * | | use \ocaml macro in new text | Paul Steckler | 2017-11-28 | |
| | | | | | ||||
| * | | | | Fix (partial) #4878: option to stop autodeclaring axiom as instance. |  Gaëtan Gilbert | 2017-11-28 | |
| |/ / / | ||||
| * | | | Merge PR #1033: Universe binder improvements | Maxime Dénès | 2017-11-28 | |
| |\ \ \ | ||||
| * | | | | Updating the current official writing of OCaml, updating Camlp4->Camlp5. |  Hugo Herbelin | 2017-11-25 | |
| | | | | | ||||
| | * | | | Allow local universe renaming in Print. | Gaëtan Gilbert | 2017-11-25 | |
| |/ / / | ||||
| | * / | use OCaml criteria for infix ops, #6212 |  Paul Steckler | 2017-11-22 | |
| |/ / | ||||
| * | | Rename coq-inferior.el -> inferior-coq.el to match provided feature. | Gaëtan Gilbert | 2017-11-19 | |
| | | | | | | | | | Fixes #4988. | |||
| * | | coq_makefile: document COQ_SRC_SUBDIRS |  Enrico Tassi | 2017-11-13 | |
| | | | ||||
| * | | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]", |  Samuel Gruetter | 2017-11-06 | |
| | | | | | | | | | | | | | not "first [ progress tac1 | progress tac2 ]". And add a missing backslash. | |||
| * | | Merge PR #1139: Add a linter. | Maxime Dénès | 2017-11-06 | |
| |\ \ | ||||
| * \ \ | Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631 | Maxime Dénès | 2017-10-27 | |
| |\ \ \ | ||||
| * | | | | Rename \Tree to \NatTree |  Johannes Kloos | 2017-10-25 | |
| | | | | | ||||
| | | * | | Put newlines at the end of files. | Gaëtan Gilbert | 2017-10-25 | |
| | | | | | ||||
| * | | | | Fix #5763: Strictly positive example is out of order. | jkloos | 2017-10-24 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | I also renamed the type to nattree (see discussion on https://github.com/coq/coq/pull/5979) to disambiguate from another, earlier example. | |||
| | * | | | Fix #4846 | Johannes Kloos | 2017-10-24 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | |||
| | * | | | Fix #5413: [unfold ... in] not documented | Johannes Kloos | 2017-10-24 | |
| | | | | | | | | | | | | | | | | | Made a description of unfold...in and moved the index entry there. | |||
| | * | | | Documentation: Add various basic constructs to the index. | Johannes Kloos | 2017-10-24 | |
| | | | | | | | | | | | | | | | | | | | | | This was mentioned in #5631 as well. Now, forall, fun and casts have index entries. | |||
| | * | | | Fix part of 'Hard to find documentation for `(...) and `{...} #5631' | Johannes Kloos | 2017-10-24 | |
| |/ / / | | | | | | | | | | | | | As discussed in the bug report, this adds `(...) and `{...} to the index. | |||
| * | | | Remove GeoProof support. | Maxime Dénès | 2017-10-11 | |
| | | | | | | | | | | | | | | | | Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq). | |||
| * | | | Merge PR #1116: Updating citing Coq in FAQ. | Maxime Dénès | 2017-10-10 | |
| |\ \ \ | |/ / |/| | | ||||
| | * | | Updating citing Coq in FAQ. | Hugo Herbelin | 2017-10-10 | |
| | | | | ||||
| * | | | Fix copyright info in reference manual. |  Théo Zimmermann | 2017-10-06 | |
| | | | | | | | | | | | | | Also simplifies the way it is presented (no need to be overly precise). | |||
| * | | | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵ | Maxime Dénès | 2017-10-05 | |
| |\ \ \ | | | | | | | | | | | | | to escape non-UTF-8 file names) | |||
| * \ \ \ | Merge PR #1080: Remove some unused parts of the reference manual. | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ | ||||
| * | | | | | [vernac] Remove `Qed exporting` syntax. |  Emilio Jesus Gallego Arias | 2017-09-29 | |
| | |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why. | |||
| | * | | | 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-22 | |
| |/ / / | ||||
| | * / | Reference manual: A few words about the file system constraints for -Q/-R. | Hugo Herbelin | 2017-09-13 | |
| |/ / | ||||
| * | | 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-11 | |
| |\ \ \ \ \ | ||||
| | | | | * | | Fix Typo in Doc for `Set Parsing Explicit` |  staffehn | 2017-09-08 | |
| | |_|_|/ / |/| | | | | ||||
| | | | * | | Fix the introduction of SSR refman chapter. | Théo Zimmermann | 2017-09-08 | |
| | |_|/ / |/| | | | ||||
| * | | | | 2 Typos in 'Add Parametric Morphism' Documentation | staffehn | 2017-09-03 | |
| | | | | | ||||
| | | * | | add option index entry for NativeCompute Profiling | Paul Steckler | 2017-09-01 | |
| | |/ / |/| | | ||||
| | | * | Fixing various typos in the Credits chapter. | Théo Zimmermann | 2017-09-01 | |
| | |/ |/| | ||||
| | * | 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-31 | |
| |\ \ \ | |_|/ |/| | | ||||
| | * | | 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-29 | |
| |\ \ \ | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |