| Commit message (Expand) | Author | Age |
* | Merge PR #540: [configure] Support for flambda flags. | Maxime Dénès | 2017-10-10 |
|\ |
|
* \ | Merge PR #768: Omega and romega know about context definitions (fix old bug 148) | Maxime Dénès | 2017-10-10 |
|\ \ |
|
| | * | [configure] Support for flambda flags. | Emilio Jesus Gallego Arias | 2017-10-10 |
| |/
|/| |
|
* | | Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on... | Maxime Dénès | 2017-10-09 |
|\ \ |
|
* | | | 8.7+beta2 CHANGES | Théo Zimmermann | 2017-10-06 |
| | * | romega: takes advantage of context variables with body | Pierre Letouzey | 2017-10-05 |
| | * | Omega now aware of context variables with bodies (in type Z or nat) (fix bug ... | Pierre Letouzey | 2017-10-05 |
| |/
|/| |
|
* | | Mention requiring extraction/funind in CHANGES | Tej Chajed | 2017-10-02 |
| * | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler | 2017-09-25 |
|/ |
|
* | Fix CHANGES after merge of PR #1025. | Théo Zimmermann | 2017-09-15 |
* | read flags from project file for Compile Buffer | Paul Steckler | 2017-09-05 |
* | move mention of native_compute profiling in CHANGES | Paul Steckler | 2017-09-01 |
* | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | Maxime Dénès | 2017-08-29 |
|\ |
|
| * | add CHANGES entry | Paul Steckler | 2017-08-18 |
* | | Correct the option for cumulativity in CHANGES | Amin Timany | 2017-08-18 |
|/ |
|
* | Use the wording suggested by Gaetan. | Théo Zimmermann | 2017-08-17 |
* | Addition suggested by Pierre-Marie. | Théo Zimmermann | 2017-08-17 |
* | Additions following Hugo's suggestions. | Théo Zimmermann | 2017-08-16 |
* | Improve wording. | Théo Zimmermann | 2017-08-16 |
* | 8.7 CHANGES | Théo Zimmermann | 2017-08-16 |
* | Porting #856 (8.6.1 CHANGES entries) to master | Théo Zimmermann | 2017-08-16 |
* | 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 |