| Commit message (Expand) | Author | Age |
* | 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 |
* | Update header of CHANGES. | Maxime Dénès | 2015-01-15 |
* | Mention guard condition in CHANGES. | Maxime Dénès | 2015-01-15 |
* | CHANGES: my recent updates to Ltac. | Arnaud Spiwack | 2015-01-14 |
* | More in CHANGES about local definitions | Pierre-Marie Pédrot | 2015-01-13 |
* | CHANGES: mention "Optimize (Heap|Proof)" | Enrico Tassi | 2015-01-10 |
* | Update + English in CHANGES | Hugo Herbelin | 2015-01-08 |
* | Start credits for 8.5. | Matthieu Sozeau | 2015-01-08 |
* | Fixed and extend bullet related info/error messages. + doc. | Pierre Courtieu | 2015-01-08 |
* | Document native_compute. | Maxime Dénès | 2015-01-08 |
* | rename: vi -> vio | Enrico Tassi | 2015-01-06 |
* | Document the new behavior of lazymatch. | Guillaume Melquiond | 2014-12-30 |
* | more CHANGES | Enrico Tassi | 2014-12-30 |
* | Minor modification of CHANGE. | Pierre Courtieu | 2014-12-23 |
* | Better doc and a few fixes for Proof using. | Enrico Tassi | 2014-12-19 |
* | In CHANGES, alerting about stronger check on notation level modifiers. | Hugo Herbelin | 2014-12-16 |
* | About now accepts hypothesis names and goal selector. | Pierre Courtieu | 2014-12-15 |
* | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu | 2014-12-12 |
* | Documenting the Set Refine Instance Mode. | Pierre-Marie Pédrot | 2014-11-30 |
* | Hopefully the last word on having "simpl f" complying with the | Hugo Herbelin | 2014-11-18 |
* | Fixing detection of occurrences in the presence of nested subterms for | Hugo Herbelin | 2014-11-18 |
* | Documenting use of colors in Coq. | Pierre-Marie Pédrot | 2014-11-17 |
* | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin | 2014-11-16 |
* | Updating CHANGES (evars as ident). | Hugo Herbelin | 2014-11-11 |
* | American spelling + layout in CHANGES. | Hugo Herbelin | 2014-11-11 |
* | Fixing careless name confusion in CHANGES. | Pierre-Marie Pédrot | 2014-11-04 |
* | Documenting the change of semantics of the replace tactic. | Pierre-Marie Pédrot | 2014-11-04 |
* | Improving elimination with indices, getting rid of intrusive residual | Hugo Herbelin | 2014-11-02 |
* | This commit introduces changes in induction and destruct. | Hugo Herbelin | 2014-10-25 |