| Commit message (Expand) | Author | Age |
* | use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language | Paul Steckler | 2017-12-05 |
* | Merge PR #890: Global universe declarations | Maxime Dénès | 2017-12-05 |
|\ |
|
* \ | Merge PR #6300: Clarify operation of sequences, fixes #6095 | Maxime Dénès | 2017-12-05 |
|\ \ |
|
* \ \ | 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 |
| |_|/
|/| | |
|
* | | | 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 |
|/ / |
|
* | | 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 |
* | coq_makefile: document COQ_SRC_SUBDIRS | Enrico Tassi | 2017-11-13 |
* | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]", | Samuel Gruetter | 2017-11-06 |
* | 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 |
| * | | Fix #4846 | Johannes Kloos | 2017-10-24 |
| * | | Fix #5413: [unfold ... in] not documented | Johannes Kloos | 2017-10-24 |
| * | | Documentation: Add various basic constructs to the index. | Johannes Kloos | 2017-10-24 |
| * | | Fix part of 'Hard to find documentation for `(...) and `{...} #5631' | Johannes Kloos | 2017-10-24 |
|/ / |
|
* / | Remove GeoProof support. | Maxime Dénès | 2017-10-11 |
|/ |
|
* | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t... | Maxime Dénès | 2017-10-05 |
|\ |
|
* \ | 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 |
| * | | 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 |
| |/
|/| |
|
| * | 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 |
|\ \ |
|
* | | | Fix obsolete description of real numerals. | Guillaume Melquiond | 2017-08-22 |
| |/
|/| |
|
| * | 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-18 |
|\ \ |
|
| | * | Add native compute profiling, BZ#5170 | Paul Steckler | 2017-08-17 |
| |/
|/| |
|