aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
...
* Merge PR #6949: Revert PR #873: New strategy based on open scopes for decidin...Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\ \
| | * Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Gravatar Maxime Dénès2018-03-09
* | | Merge PR #6923: Export optionsGravatar Maxime Dénès2018-03-09
|\ \ \ | |_|/ |/| |
| | * Documentation for Cumulativity Weak Constraints.Gravatar Gaëtan Gilbert2018-03-09
* | | Merge PR #6480: Allow Prop as source for coercionsGravatar Maxime Dénès2018-03-09
|\ \ \ | |_|/ |/| |
* | | Merge PR #6820: Tacticals assert_fails and assert_succeedsGravatar Maxime Dénès2018-03-09
|\ \ \
| | | * Documenting the Export modifier for options in CHANGES.Gravatar Pierre-Marie Pédrot2018-03-09
| |_|/ |/| |
| | * doc and changes for coercion from prop/typeGravatar charguer2018-03-09
| |/ |/|
* | Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for fiat-cry...Gravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Gravatar Maxime Dénès2018-03-08
|\ \ \
* \ \ \ Merge PR #6743: Add notation {x & P} for sigTGravatar Maxime Dénès2018-03-08
|\ \ \ \
* \ \ \ \ Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \
* | | | | | | [vernac] Warn when using “Require” in a sectionGravatar Vincent Laporte2018-03-07
* | | | | | | Merge PR #6744: Add String.concatGravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \
| | | | | | * | Add CHANGES and man entry for coqdep learning _CoqProject.Gravatar Gaëtan Gilbert2018-03-06
| | | | | * | | An experimental 'Show Extraction' command (grant feature wish #4129)Gravatar Pierre Letouzey2018-03-06
| | | | | |/ /
* | | | | | | CHANGES and tests for with Definition @{univs}Gravatar Gaëtan Gilbert2018-03-05
| | | * | | | Deprecate Focus and Unfocus.Gravatar Théo Zimmermann2018-03-05
| | | | |/ / | | | |/| |
* | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
| * | | | | | CHANGES entry for #6791.Gravatar Théo Zimmermann2018-03-02
| | |_|/ / / | |/| | | |
* / | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
|/ / / / /
| | | | * Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Gravatar Hugo Herbelin2018-02-28
| * | | | Add String.concatGravatar Jason Gross2018-02-24
|/ / / /
* | | | Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ | |_|_|/ |/| | |
* | | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \ \ \
| | * | | Add CHANGES entry for decimals in preludeGravatar Jason Gross2018-02-20
* | | | | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
* | | | | More flexibility in locating or referring to a notation.Gravatar Hugo Herbelin2018-02-20
* | | | | A first step at refreshing and documenting the new feature.Gravatar Hugo Herbelin2018-02-20
* | | | | Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
| |/ / / |/| | |
| | * | Implement name mangling optionGravatar Jasper Hugunin2018-02-17
| |/ / |/| |
| * | Extend `zify_N` with knowledge about `N.pred`Gravatar Joachim Breitner2018-02-14
* | | CHANGES for 8.7.2.Gravatar Théo Zimmermann2018-02-14
|/ /
* | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)Gravatar Maxime Dénès2018-02-14
|\ \
| * | Add CHANGES entry for #1047Gravatar Tej Chajed2018-02-13
| | * Add notation {x & P} for sigTGravatar Tej Chajed2018-02-12
| |/
* / CHANGES for universe varianceGravatar Gaëtan Gilbert2018-02-12
|/
* 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
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 21:29:26 +0000