aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* [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
|
* Merge PR #6949: Revert PR #873: New strategy based on open scopes for ↵Gravatar Maxime Dénès2018-03-09
|\ | | | | | | deciding…
* \ 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 ↵Gravatar Maxime Dénès2018-03-09
| | | | | | | | | | | | | | | | | | | | | notation to use among several of them" This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
* | | 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 ↵Gravatar Maxime Dénès2018-03-09
|\ \ | | | | | | | | | fiat-crypto/OSX
* \ \ Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵Gravatar Maxime Dénès2018-03-08
|\ \ \ | | | | | | | | | | | | wish #4129)
* \ \ \ 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
| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 00:03:02 +0000