aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* 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.
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
| | | | | | | | | | | | | | | - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
* Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ↵Gravatar Pierre Boutillier2015-02-28
| | | | r15439 as we were talking at that time)
* CHANGES: Info command + info_auto currently broken.Gravatar Arnaud Spiwack2015-02-24
|
* Undo: back to 8.4 semantics (Close #3514)Gravatar Enrico Tassi2015-02-15
| | | | Only tactics are taken into account.
* Note about "Undo. Undo." in CHANGESGravatar Enrico Tassi2015-02-15
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 00:19:23 +0000