aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* 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
|
* 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
| | | | | | |
* | | | | | | 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
| | | | | |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
* | | | | | | 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
|/ / / / / | | | | | | | | | | | | | | | Noticed by Sigurd Schneider.
| | | | * Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Gravatar Hugo Herbelin2018-02-28
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 07:21:37 +0000