| Commit message (Expand) | Author | Age |
* | Merge PR #925: Document Extraction TestCompile | Maxime Dénès | 2017-08-01 |
|\ |
|
| * | Extraction TestCompile documented + mentionned in CHANGES | Pierre Letouzey | 2017-07-27 |
* | | Adding support for recursive notations of the form "x , .. , y , z". | Hugo Herbelin | 2017-07-26 |
|/ |
|
* | Add an entry to CHANGES about timing in coq_makefile | Jason Gross | 2017-07-11 |
* | Update CHANGES with inversion_sigma entry | Jason Gross | 2017-06-30 |
* | Merge PR#774: [ide] Add route_id parameter to query call. | Maxime Dénès | 2017-06-20 |
|\ |
|
| * | [ide] Add route_id parameter to query call. | Emilio Jesus Gallego Arias | 2017-06-18 |
* | | Document cumulativity for inductive types | Amin Timany | 2017-06-16 |
|/ |
|
* | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey | 2017-06-13 |
* | Merge PR#709: Bytecode compilation apart from 'make world', again | Maxime Dénès | 2017-06-12 |
|\ |
|
| * | mention 'make world' without 'byte' in CHANGES + 2 minor suggestions | Pierre Letouzey | 2017-06-01 |
* | | Merge PR#449: make specialize smarter (bug 5370). | Maxime Dénès | 2017-06-01 |
|\ \ |
|
| * | | Tests for new specialize feature + CHANGES. | Pierre Courtieu | 2017-05-31 |
| |/ |
|
* / | Documentation for eassert, eenough, epose proof, eset, eremember, epose. | Hugo Herbelin | 2017-05-30 |
|/ |
|
* | Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings | Maxime Dénès | 2017-05-25 |
|\ |
|
* \ | Merge PR#406: coq makefile2 | Maxime Dénès | 2017-05-25 |
|\ \ |
|
| * | | enters coq_makefile2 | Enrico Tassi | 2017-05-23 |
* | | | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias | 2017-05-23 |
|/ / |
|
| * | Clarifying the interpretation path for the "constr_with_binding" argument. | Hugo Herbelin | 2017-05-22 |
|/ |
|
* | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès | 2017-05-17 |
|\ |
|
* | | Aligning on standard layout of CHANGES. | Hugo Herbelin | 2017-05-13 |
| * | Documenting Printing Compact Contexts + CHANGES | Pierre Courtieu | 2017-05-11 |
* | | Tentative note in CHANGES about now applying βι while typing "match" branches. | Hugo Herbelin | 2017-04-27 |
|/ |
|
* | CHANGES entry for #545. | Maxime Dénès | 2017-04-19 |
* | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | 2017-04-11 |
|\ |
|
| * | Documenting the changes introduced by the EConstr branch. | Pierre-Marie Pédrot | 2017-04-10 |
* | | [camlpX] Enrico's changes to camlp4 removal. | Emilio Jesus Gallego Arias | 2017-04-07 |
|/ |
|
* | Merge PR#455: Farewell decl_mode | Maxime Dénès | 2017-04-06 |
|\ |
|
* | | Document the changes to IZR. | Guillaume Melquiond | 2017-03-22 |
| * | Farewell decl_mode | Enrico Tassi | 2017-03-07 |
* | | CHANGES: choice over setoids and prop. ext. | Hugo Herbelin | 2017-03-03 |
|/ |
|
* | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-01-19 |
|\ |
|
| * | A few words in CHANGES. | Maxime Dénès | 2016-12-07 |
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-30 |
|\| |
|
| * | Fix some documentation typos. | Guillaume Melquiond | 2016-11-24 |
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-18 |
|\| |
|
| * | [doc] Mention XML protocol on changes. | Emilio Jesus Gallego Arias | 2016-11-16 |
| * | Remove the list of bug fixes from CHANGES. | Maxime Dénès | 2016-11-14 |
| * | Update CHANGES and credits for 8.6beta1. | Maxime Dénès | 2016-11-10 |
| * | Mention notypeclasses refine in CHANGES | Matthieu Sozeau | 2016-11-07 |
| * | CHANGES for this branch. | Matthieu Sozeau | 2016-11-07 |
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-29 |
|\| |
|
| * | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-26 |
| |\ |
|
| | * | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | Maxime Dénès | 2016-10-25 |
| | * | Update CHANGES. | Maxime Dénès | 2016-10-25 |
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-12 |
|\| | |
|
* | | | Allocating a section in CHANGES for changes specific to 8.7. | Hugo Herbelin | 2016-10-12 |
| * | | Tentatively preparing to add changes specific to v8.7 (see PR #275). | Hugo Herbelin | 2016-10-12 |
|/ / |
|
* | | Report about changes of semantics of auto as an ltac argument (see #4966). | Hugo Herbelin | 2016-10-08 |
* | | Remove the Set Verbose Compat option and turn the warning on by default. | Maxime Dénès | 2016-10-06 |