| Commit message (Expand) | Author | Age |
* | Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction) | Hugo Herbelin | 2015-12-05 |
* | Fix CHANGES. | Hugo Herbelin | 2015-12-05 |
* | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | 2015-12-02 |
* | Fix bug #4433, removing hack on evars appearing in a pattern from a | Matthieu Sozeau | 2015-11-19 |
* | Update CHANGES | Jason Gross | 2015-11-12 |
* | Fix bug #3735: interpretation of "->" in Program follows the standard one. | Matthieu Sozeau | 2015-11-11 |
* | Update version numbers and magic numbers for 8.5beta3 release. | Maxime Dénès | 2015-11-05 |
* | Hint Cut documentation and cleanup of printing (was duplicated and | Matthieu Sozeau | 2015-11-04 |
* | Adding syntax "Show id" to show goal named id (shelved or not). | Hugo Herbelin | 2015-11-02 |
* | Mention bug 3199 fix as a source of incompatibilities. | Matthieu Sozeau | 2015-10-21 |
* | Documenting the option "Strict Universe Declaration" in CHANGES. | Pierre-Marie Pédrot | 2015-10-19 |
* | Fix some typos. | Guillaume Melquiond | 2015-10-13 |
* | Remove the "exists" overrides from Program. (Fix bug #4360) | Guillaume Melquiond | 2015-10-07 |
* | Make -load-vernac-object respect the loadpath. | Guillaume Melquiond | 2015-09-28 |
* | The -require option now accepts a logical path instead of a physical one. | Pierre-Marie Pédrot | 2015-09-25 |
* | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot | 2015-09-25 |
* | Explain new flags for native_compute in CHANGES. | Maxime Dénès | 2015-09-16 |
* | New option "Unset Bracketing Last Introduction Pattern" for preserving | Hugo Herbelin | 2015-09-08 |
* | Granting Jason's request for an ad hoc compatibility option on | Hugo Herbelin | 2015-08-02 |
* | Documenting change of behavior of apply when the lemma is a tuple and | Hugo Herbelin | 2015-08-02 |
* | Rewording about how to upgrade on failing calls to constructor. | Hugo Herbelin | 2015-07-10 |
* | CHANGES: grammatical correction, suggested by Jason Gross on Bugzilla. | Maxime Dénès | 2015-07-10 |
* | More precise rewording about asymmetric patterns. | Hugo Herbelin | 2015-07-05 |
* | Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" | Lionel Rieg | 2015-06-26 |
* | Fixed CHANGES to reflect -color option. | Pierre Courtieu | 2015-05-18 |
* | Adding an option -w to control Coq warning output. | Pierre-Marie Pédrot | 2015-05-14 |
* | Safer typing primitives. | Pierre-Marie Pédrot | 2015-05-13 |
* | Documenting the Loose Hint Behavior flag. | Pierre-Marie Pédrot | 2015-05-13 |
* | Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for | Hugo Herbelin | 2015-05-09 |
* | Fix documentation of Redirect | Enrico Tassi | 2015-05-04 |
* | More precise numbers about Benjamin's fix for the VM. | Maxime Dénès | 2015-04-22 |
* | Update CHANGES | Matthieu Sozeau | 2015-04-22 |
* | Removing references to -I -as from CHANGES. | Pierre-Marie Pédrot | 2015-04-07 |
* | Accomodating #4166 (providing "Require Import OmegaTactic" as a | Hugo Herbelin | 2015-04-01 |
* | Announcing * and ** which were not official yet in 8.4. | Hugo Herbelin | 2015-03-22 |
* | Aliasing give_up with admit | Enrico Tassi | 2015-03-22 |
* | CHANGES: more correct equivalent to "constructor tac" syntax. | Arnaud Spiwack | 2015-03-13 |
* | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi | 2015-03-11 |
* | Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ... | Pierre Boutillier | 2015-02-28 |
* | CHANGES: Info command + info_auto currently broken. | Arnaud Spiwack | 2015-02-24 |
* | Undo: back to 8.4 semantics (Close #3514) | Enrico Tassi | 2015-02-15 |
* | Note about "Undo. Undo." in CHANGES | Enrico Tassi | 2015-02-15 |
* | Document the behavior change of Instance wrt {|...|}. (Fix for bug #3749) | Guillaume Melquiond | 2015-02-15 |
* | Document the issue with trivial inductive types. (Workaround for bug #3984) | Guillaume Melquiond | 2015-02-13 |
* | Fix typos about .vio files (thanks Arthur for spotting them) | Enrico Tassi | 2015-02-12 |
* | Updating CHANGES (grammar, thanks to AS for pointing it out) + | Hugo Herbelin | 2015-01-24 |
* | Typos, grammar, layout in CHANGES (continued). | Hugo Herbelin | 2015-01-23 |
* | Typos, grammar, layout in CHANGES. | Hugo Herbelin | 2015-01-23 |
* | Documenting the removal of coercions between sig, sigT, sig2, | Hugo Herbelin | 2015-01-16 |
* | Move explanations about primitive projections to the manual. | Matthieu Sozeau | 2015-01-15 |