aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
| | | | | | | | | | | | | | | preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual.
* Mention problems with fix of #4582 in CHANGES.Gravatar Maxime Dénès2016-04-22
|
* Mention #4548 (fixed) in CHANGES.Gravatar Maxime Dénès2016-04-22
|
* Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
| | | | | while eta-expanding a notation) + a more serious variant of it (alpha-conversion incorrect wrt eta-expansion).
* Add changelog for 8.5pl1 after the fact.Gravatar Maxime Dénès2016-04-17
| | | | Will be displayed on the website, but not part of the package.
* Reporting about the new tactical unshelve.Gravatar Hugo Herbelin2016-01-12
|
* Update version numbers and magic numbers for 8.5rc1 release.Gravatar Maxime Dénès2015-12-16
|
* Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Gravatar Guillaume Melquiond2015-12-16
|
* Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
| | | | | | The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account.
* Updating CHANGES with an incompatibility.Gravatar Hugo Herbelin2015-12-14
|
* Flag -compat 8.4 now loads Coq.Compat.Coq84.Gravatar Maxime Dénès2015-12-14
|
* Document removal of Set Virtual Machine and -vm in CHANGES.Gravatar Maxime Dénès2015-12-11
|
* Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
| | | | Marking it as experimental.
* Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Gravatar Hugo Herbelin2015-12-05
| | | | | | | | based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal.
* Fix CHANGES.Gravatar Hugo Herbelin2015-12-05
|
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
|
* Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
| | | | | constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
* Update CHANGESGravatar Jason Gross2015-11-12
| | | | Mention compatibility file.
* Fix bug #3735: interpretation of "->" in Program follows the standard one.Gravatar Matthieu Sozeau2015-11-11
|
* Update version numbers and magic numbers for 8.5beta3 release.Gravatar Maxime Dénès2015-11-05
|
* Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
| | | | inconsistent).
* Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
|
* Mention bug 3199 fix as a source of incompatibilities.Gravatar Matthieu Sozeau2015-10-21
|
* Documenting the option "Strict Universe Declaration" in CHANGES.Gravatar Pierre-Marie Pédrot2015-10-19
|
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
|
* Remove the "exists" overrides from Program. (Fix bug #4360)Gravatar Guillaume Melquiond2015-10-07
|
* Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
| | | | | | | | | | This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq.
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
|
* Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
|
* Explain new flags for native_compute in CHANGES.Gravatar Maxime Dénès2015-09-16
|
* New option "Unset Bracketing Last Introduction Pattern" for preservingGravatar Hugo Herbelin2015-09-08
| | | | | | | | compatibility with the non uniform behavior that "intros [] []" on "A*B->C*D->E" automatically introduces A and B but leaves C and D in the goal. Kept unset in 8.5 but planned to be set in 8.6.
* Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
| | | | | | | considering trivial unifications "?x = t" in tactics working under conjunctions (see #3545). Also updating and fixing wrong comments in test apply.v.
* Documenting change of behavior of apply when the lemma is a tuple andGravatar Hugo Herbelin2015-08-02
| | | | applying a component of the tuple.
* Rewording about how to upgrade on failing calls to constructor.Gravatar Hugo Herbelin2015-07-10
|
* CHANGES: grammatical correction, suggested by Jason Gross on Bugzilla.Gravatar Maxime Dénès2015-07-10
|
* More precise rewording about asymmetric patterns.Gravatar Hugo Herbelin2015-07-05
|
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
|
* Fixed CHANGES to reflect -color option.Gravatar Pierre Courtieu2015-05-18
|
* Adding an option -w to control Coq warning output.Gravatar Pierre-Marie Pédrot2015-05-14
| | | | | | | For now, warnings are still ignored by default, but this may change. This commit at least allows to print them whenever desired. The -w syntax is also opened to future additions to further control the display of warnings.
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
| | | | | | | | | | | | | | | | Some functions from pretyping/typing.ml and their derivatives were potential source of evarmap leaks, as they dropped their resulting evarmap. This commit clarifies the situation by renaming them according to a unsafe_* scheme. Their sound variant is likewise renamed to their old name. The following renamings were made. - Typing.type_of -> unsafe_type_of - Typing.e_type_of -> type_of - A new e_type_of function that matches the e_ prefix policy - Tacmach.pf_type_of -> pf_unsafe_type_of - A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated.
* Documenting the Loose Hint Behavior flag.Gravatar Pierre-Marie Pédrot2015-05-13
|
* Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forGravatar Hugo Herbelin2015-05-09
| | | | preserving compatibility of subst after #4214 being solved.
* Fix documentation of RedirectGravatar Enrico Tassi2015-05-04
|
* More precise numbers about Benjamin's fix for the VM.Gravatar Maxime Dénès2015-04-22
|
* Update CHANGESGravatar Matthieu Sozeau2015-04-22
|
* Removing references to -I -as from CHANGES.Gravatar Pierre-Marie Pédrot2015-04-07
|
* Accomodating #4166 (providing "Require Import OmegaTactic" as aGravatar Hugo Herbelin2015-04-01
| | | | replacement for 8.4's "Require Omega").
* Announcing * and ** which were not official yet in 8.4.Gravatar Hugo Herbelin2015-03-22
|
* Aliasing give_up with admitGravatar Enrico Tassi2015-03-22
|
* CHANGES: more correct equivalent to "constructor tac" syntax.Gravatar Arnaud Spiwack2015-03-13
| | | | As mentionne in #3969, using "once (constructor;tac)" leads in exponential blowups, whereas "[> once (constructor;tac) ..]" does not.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 15:11:38 +0000