aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Merge PR #873: New strategy based on open scopes for deciding which notation ...Gravatar Maxime Dénès2017-12-07
|\
* | Update CHANGESGravatar Matthieu Sozeau2017-12-01
* | Merge PR #6276: Coqchk accepts filenamesGravatar Maxime Dénès2017-12-01
|\ \
* | | Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| * | Documenting the possibility to pass filenames to coqchk.Gravatar Pierre-Marie Pédrot2017-11-29
|/ /
| * Selecting which notation to print based on current stack of scope.Gravatar Hugo Herbelin2017-11-27
|/
* Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
* Moving bug numbers to BZ# format in the CHANGES file.Gravatar Théo Zimmermann2017-10-19
* Merge PR #540: [configure] Support for flambda flags.Gravatar Maxime Dénès2017-10-10
|\
* \ Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Gravatar Maxime Dénès2017-10-10
|\ \
| | * [configure] Support for flambda flags.Gravatar Emilio Jesus Gallego Arias2017-10-10
| |/ |/|
* | Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...Gravatar Maxime Dénès2017-10-09
|\ \
* | | 8.7+beta2 CHANGESGravatar Théo Zimmermann2017-10-06
| | * romega: takes advantage of context variables with bodyGravatar Pierre Letouzey2017-10-05
| | * Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...Gravatar Pierre Letouzey2017-10-05
| |/ |/|
* | Mention requiring extraction/funind in CHANGESGravatar Tej Chajed2017-10-02
| * BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsGravatar Paul Steckler2017-09-25
|/
* Fix CHANGES after merge of PR #1025.Gravatar Théo Zimmermann2017-09-15
* read flags from project file for Compile BufferGravatar Paul Steckler2017-09-05
* move mention of native_compute profiling in CHANGESGravatar Paul Steckler2017-09-01
* Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Gravatar Maxime Dénès2017-08-29
|\
| * add CHANGES entryGravatar Paul Steckler2017-08-18
* | Correct the option for cumulativity in CHANGESGravatar Amin Timany2017-08-18
|/
* Use the wording suggested by Gaetan.Gravatar Théo Zimmermann2017-08-17
* Addition suggested by Pierre-Marie.Gravatar Théo Zimmermann2017-08-17
* Additions following Hugo's suggestions.Gravatar Théo Zimmermann2017-08-16
* Improve wording.Gravatar Théo Zimmermann2017-08-16
* 8.7 CHANGESGravatar Théo Zimmermann2017-08-16
* Porting #856 (8.6.1 CHANGES entries) to masterGravatar Théo Zimmermann2017-08-16
* Merge PR #925: Document Extraction TestCompileGravatar Maxime Dénès2017-08-01
|\
| * Extraction TestCompile documented + mentionned in CHANGESGravatar Pierre Letouzey2017-07-27
* | Adding support for recursive notations of the form "x , .. , y , z".Gravatar Hugo Herbelin2017-07-26
|/
* Add an entry to CHANGES about timing in coq_makefileGravatar Jason Gross2017-07-11
* Update CHANGES with inversion_sigma entryGravatar Jason Gross2017-06-30
* Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\
| * [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
* | Document cumulativity for inductive typesGravatar Amin Timany2017-06-16
|/
* BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
* Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\
| * mention 'make world' without 'byte' in CHANGES + 2 minor suggestionsGravatar Pierre Letouzey2017-06-01
* | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \
| * | Tests for new specialize feature + CHANGES.Gravatar Pierre Courtieu2017-05-31
| |/
* / Documentation for eassert, eenough, epose proof, eset, eremember, epose.Gravatar Hugo Herbelin2017-05-30
|/
* Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\
* \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \
| * | enters coq_makefile2Gravatar Enrico Tassi2017-05-23
* | | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
|/ /
| * Clarifying the interpretation path for the "constr_with_binding" argument.Gravatar Hugo Herbelin2017-05-22
|/
* Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\
* | Aligning on standard layout of CHANGES.Gravatar Hugo Herbelin2017-05-13