aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2018-03-09Merge PR #6949: Revert PR #873: New strategy based on open scopes for decidin...Maxime Dénès
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Maxime Dénès
2018-03-09Merge PR #6923: Export optionsMaxime Dénès
2018-03-09Documentation for Cumulativity Weak Constraints.Gaëtan Gilbert
2018-03-09Merge PR #6480: Allow Prop as source for coercionsMaxime Dénès
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-03-09Documenting the Export modifier for options in CHANGES.Pierre-Marie Pédrot
2018-03-09doc and changes for coercion from prop/typecharguer
2018-03-09Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for fiat-cry...Maxime Dénès
2018-03-08Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Maxime Dénès
2018-03-08Merge PR #6743: Add notation {x & P} for sigTMaxime Dénès
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-07[vernac] Warn when using “Require” in a sectionVincent Laporte
2018-03-07Merge PR #6744: Add String.concatMaxime Dénès
2018-03-06Add CHANGES and man entry for coqdep learning _CoqProject.Gaëtan Gilbert
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
2018-03-05CHANGES and tests for with Definition @{univs}Gaëtan Gilbert
2018-03-05Deprecate Focus and Unfocus.Théo Zimmermann
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-02CHANGES entry for #6791.Théo Zimmermann
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
2018-02-28Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Hugo Herbelin
2018-02-24Add String.concatJason Gross
2018-02-24Merge PR #6599: Decimals in preludeMaxime Dénès
2018-02-21Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Maxime Dénès
2018-02-20Add CHANGES entry for decimals in preludeJason Gross
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-17Implement name mangling optionJasper Hugunin
2018-02-14Extend `zify_N` with knowledge about `N.pred`Joachim Breitner
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-12Add notation {x & P} for sigTTej 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 05:17:47 +0000