aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Merge PR #7920: Generic syntax for attributesGravatar Maxime Dénès2018-07-09
|\
* | Mention the removal of Emacs modes in CHANGES.Gravatar Théo Zimmermann2018-07-08
* | Merge PR #7921: Archive the `gallina` toolGravatar Maxime Dénès2018-07-07
|\ \
| | * Document attributes.Gravatar Vincent Laporte2018-07-03
| |/ |/|
* | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\ \
| * | hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
* | | Document option Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
|/ /
* | CHANGES for 8.8.1.Gravatar Théo Zimmermann2018-06-28
* | Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \
* | | Fix #7723: vm_compute segfaults with universe polymorphismGravatar Maxime Dénès2018-06-27
| | * Archive the `gallina` toolGravatar Vincent Laporte2018-06-25
| |/ |/|
| * Added mention of mutual records to CHANGES.Gravatar Pierre-Marie Pédrot2018-06-24
|/
* [ssr] implement {}/v as a short hand for {v}/v when v is an idGravatar Enrico Tassi2018-06-22
* [ssr] simplify delayed clearsGravatar Enrico Tassi2018-06-22
* Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
* Fix #7615: Functor inlining drops universe substitution.Gravatar Pierre-Marie Pédrot2018-06-07
* Make direct invocations of `simple apply` obey `Opaque` directive.Gravatar Maxime Dénès2018-06-05
* Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\
* \ Merge PR #7486: Update old parts of CHANGES to use current bug numbers.Gravatar Hugo Herbelin2018-06-04
|\ \
| | * Documenting the deprecation.Gravatar Pierre-Marie Pédrot2018-06-04
| |/ |/|
* | Add CHANGES entryGravatar Maxime Dénès2018-05-28
* | [tactics] Remove anonymous fix/cofix form.Gravatar Emilio Jesus Gallego Arias2018-05-24
* | [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
* | Document nested proofs and associated option.Gravatar Théo Zimmermann2018-05-17
| * Update old parts of CHANGES to use current bug numbers.Gravatar Théo Zimmermann2018-05-11
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-20 07:13:51 +0000