aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Merge PR #6629: Archive COMPATIBILITYGravatar Maxime Dénès2018-01-23
|\
| * Move the mention of the removal of Qed exporting at the right place.Gravatar Théo Zimmermann2018-01-22
* | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\ \
* | | add flash infos about wrap, not found, no. of replacements, no. of finds, iss...Gravatar Paul Steckler2018-01-18
| |/ |/|
* | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \
| | * Add CHANGES entryGravatar Jasper Hugunin2018-01-17
| * | Add CHANGES entryGravatar Jasper Hugunin2018-01-17
| |/
* | Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\ \ | |/ |/|
| * Documentation and CHANGES for bracket with goal selector.Gravatar Théo Zimmermann2018-01-05
* | add optimize_heap tactic for #6488Gravatar Paul Steckler2018-01-03
|/
* Merge PR #6377: Removal of the FAQ LaTex document.Gravatar Maxime Dénès2017-12-20
|\
* \ Merge PR #6381: A version of [time] that works on constr evaluationGravatar Maxime Dénès2017-12-18
|\ \
* \ \ Merge PR #6380: Add tactics to reset and display the Ltac profileGravatar Maxime Dénès2017-12-18
|\ \ \
* \ \ \ Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...Gravatar Maxime Dénès2017-12-18
|\ \ \ \
| | | | * Removing the FAQ, which has been moved to the GitHub wiki for thisGravatar Matt Quinn2017-12-18
* | | | | Merge PR #6429: 8.7.1 CHANGES.Gravatar Maxime Dénès2017-12-15
|\ \ \ \ \
| | | | * | Add documentation for time_constrGravatar Jason Gross2017-12-14
| | | |/ /
| | | * / Add doc+changelog entries for new LtacProf tacticsGravatar Jason Gross2017-12-14
| |_|/ / |/| | |
| * | | 8.7.1 CHANGES.Gravatar Théo Zimmermann2017-12-14
* | | | In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
|/ / /
* | | Merge PR #873: New strategy based on open scopes for deciding which notation ...Gravatar Maxime Dénès2017-12-07
|\ \ \
| | * | use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguageGravatar Paul Steckler2017-12-05
| |/ / |/| |
* | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 01:32:29 +0000