aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2018-02-20Notations: Adding modifiers to tell which kind of binder a constr can parse.Hugo Herbelin
2018-02-20More flexibility in locating or referring to a notation.Hugo Herbelin
2018-02-20A first step at refreshing and documenting the new feature.Hugo Herbelin
2018-02-20Adding support for parsing subterms of a notation as "pattern".Hugo Herbelin
2018-02-14CHANGES for 8.7.2.Théo Zimmermann
2018-02-14Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)Maxime Dénès
2018-02-13Add CHANGES entry for #1047Tej Chajed
2018-02-12CHANGES for universe varianceGaëtan Gilbert
2018-01-23Merge PR #6629: Archive COMPATIBILITYMaxime Dénès
2018-01-22Move the mention of the removal of Qed exporting at the right place.Théo Zimmermann
2018-01-22Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Maxime Dénès
2018-01-18add flash infos about wrap, not found, no. of replacements, no. of finds, iss...Paul Steckler
2018-01-18Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Maxime Dénès
2018-01-17Add CHANGES entryJasper Hugunin
2018-01-17Add CHANGES entryJasper Hugunin
2018-01-16Merge PR #6551: Bracket with goal selectorMaxime Dénès
2018-01-05Documentation and CHANGES for bracket with goal selector.Théo Zimmermann
2018-01-03add optimize_heap tactic for #6488Paul Steckler
2017-12-20Merge PR #6377: Removal of the FAQ LaTex document.Maxime Dénès
2017-12-18Merge PR #6381: A version of [time] that works on constr evaluationMaxime Dénès
2017-12-18Merge PR #6380: Add tactics to reset and display the Ltac profileMaxime Dénès
2017-12-18Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...Maxime Dénès
2017-12-18Removing the FAQ, which has been moved to the GitHub wiki for thisMatt Quinn
2017-12-15Merge PR #6429: 8.7.1 CHANGES.Maxime Dénès
2017-12-14Add documentation for time_constrJason Gross
2017-12-14Add doc+changelog entries for new LtacProf tacticsJason Gross
2017-12-148.7.1 CHANGES.Théo Zimmermann
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-12-07Merge PR #873: New strategy based on open scopes for deciding which notation ...Maxime Dénès
2017-12-05use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguagePaul Steckler
2017-12-01Update CHANGESMatthieu Sozeau
2017-12-01Merge PR #6276: Coqchk accepts filenamesMaxime Dénès
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-11-29Documenting the possibility to pass filenames to coqchk.Pierre-Marie Pédrot
2017-11-27Selecting which notation to print based on current stack of scope.Hugo Herbelin
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
2017-10-19Moving bug numbers to BZ# format in the CHANGES file.Théo Zimmermann
2017-10-10Merge PR #540: [configure] Support for flambda flags.Maxime Dénès
2017-10-10Merge 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-09Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...Maxime Dénès
2017-10-068.7+beta2 CHANGESThéo Zimmermann
2017-10-05romega: takes advantage of context variables with bodyPierre Letouzey
2017-10-05Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...Pierre Letouzey
2017-10-02Mention requiring extraction/funind in CHANGESTej Chajed
2017-09-25BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsPaul Steckler
2017-09-15Fix CHANGES after merge of PR #1025.Théo Zimmermann
2017-09-05read flags from project file for Compile BufferPaul Steckler
2017-09-01move mention of native_compute profiling in CHANGESPaul Steckler
2017-08-29Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 09:07:56 +0000