aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Document nested proofs and associated option.Gravatar Théo Zimmermann2018-05-17
* Notations: advertize that distinct "only parsing"/"only printing" rules work.Gravatar Hugo Herbelin2018-05-11
* Make "intro"/"intros" progress on existential variables.Gravatar Hugo Herbelin2018-05-02
* Strict focusing using Default Goal Selector.Gravatar Gaëtan Gilbert2018-04-29
* Merge PR #7244: Making tactic-in-term aware of "Set Ltac Debug"Gravatar Pierre-Marie Pédrot2018-04-23
|\
* | Fix typo in CHANGES.Gravatar Maxime Dénès2018-04-16
* | Mention other deprecations and fixes in CHANGESGravatar Maxime Dénès2018-04-16
* | CHANGES: document COQFLAGS changeGravatar Ralf Jung2018-04-16
* | Merge PR #7200: [ltac] Deprecate nameless fix/cofix.Gravatar Maxime Dénès2018-04-16
|\ \
* | | Add missing CHANGES entry for #6169.Gravatar Théo Zimmermann2018-04-14
| | * Making tactic-in-term aware of "Set Ltac Debug".Gravatar Hugo Herbelin2018-04-13
| |/ |/|
| * [ltac] Deprecate nameless fix/cofix.Gravatar Emilio Jesus Gallego Arias2018-04-13
|/
* Merge PR #7103: Fix #7101: STM delegation policy brokenGravatar Enrico Tassi2018-04-09
|\
* | Fix #6404 - Print tactics called by ML tacticsGravatar Jason Gross2018-04-02
* | Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Gravatar Pierre-Marie Pédrot2018-04-01
|\ \
* | | Add CHANGES for removing Implicit Arguments and Arguments ScopeGravatar Jasper Hugunin2018-03-30
| * | Supporting fix/cofix in Ltac pattern-matching (wish #7092).Gravatar Hugo Herbelin2018-03-28
|/ /
| * Fix #7101: STM delegation policy brokenGravatar Maxime Dénès2018-03-28
|/
* Merge PR #7018: Fix typo in CHANGES.Gravatar Maxime Dénès2018-03-23
|\
* | update CHANGESGravatar Enrico Tassi2018-03-23
| * Fix typo in CHANGES.Gravatar Théo Zimmermann2018-03-19
|/
* Add some missing entries in CHANGESGravatar Maxime Dénès2018-03-15
* [doc] Document removal of deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-09
* 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
|\ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 20:13:25 +0000