aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* Remove declare_object for SsrHave NoTCResolution.Gravatar Maxime Dénès2018-07-19
| | | | | | | IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like `Global Set SsrHave NoTCResolution`. I don't think it is needed (just let the user write the desired locality), but if it is, the right way of doing it is to let clients of Goptions specify a default locality.
* Remove fourier pluginGravatar Maxime Dénès2018-07-17
| | | | As stated in the manual, the fourier tactic is subsumed by lra.
* Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | We make it possible to deprecate tactics defined by `Ltac`, `Tactic Notation` or ML. For the first two variants, we anticipate the syntax of attributes: `#[deprecated(since = "XX", note = "YY")]` In ML, the syntax is: ``` let reflexivity_depr = let open CWarnings in { since = "8.5"; note = "Use admit instead." } TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END ``` A warning is shown at the point where the tactic is used (either a direct call or when defining another tactic): Tactic `foo` is deprecated since XX. YY YY is typically meant to be "Use bar instead.".
* 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
* | | 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
| | | | | | | | | | | | Was revealing a critical bug in VM universe handling introduced in 8.5.
| | * 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
| | | | | - we always rename - we compile {clear}/view to /view{clear}
* Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
| | | | | The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
* Fix #7615: Functor inlining drops universe substitution.Gravatar Pierre-Marie Pédrot2018-06-07
| | | | | | | We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case.
* Make direct invocations of `simple apply` obey `Opaque` directive.Gravatar Maxime Dénès2018-06-05
| | | | | When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues.
* 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
| | | | | | | | | | | | | | | | | | | | We remove the `fix N / cofix N` forms from the tactic language. This way, these tactics don't depend anymore on the proof context, in particular on the proof name, which seems like a fragile practice. Apart from the concerns wrt maintenability of proof scripts, this also helps making the "proof state" functional; as we don't have to propagate the proof name to the tactic layer.
* | [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
* | 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
| | | | | | | | | | | | We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
* 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
| | | | | | | | | | | | Fixes #7243.
| | * 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
|/ | | | | | | | | | | | LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171.
* Merge PR #7103: Fix #7101: STM delegation policy brokenGravatar Enrico Tassi2018-04-09
|\ | | | | | | | | # Conflicts: # CHANGES
* | 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
|/ / | | | | | | | | This is done by not failing for fix/cofix while translating from glob_constr to constr_pattern.
| * Fix #7101: STM delegation policy brokenGravatar Maxime Dénès2018-03-28
|/ | | | | I make here a minimal fix, but a lot of cleaning should be done around Aux_file handling, including removing some code from the kernel.
* 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
|/ | | | [skip ci]
* 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
|