| Commit message (Expand) | Author | Age |
* | 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 |
* | Documenting some incompatibilities in (non) Import of ML tactics, | Hugo Herbelin | 2014-10-24 |
* | Addressing report #3279 (inconsistency of behavior of the -> and <- | Hugo Herbelin | 2014-10-24 |
* | CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defin... | Arnaud Spiwack | 2014-10-22 |
* | Mentioning incompatibility shown in #3718 and coming from #3050 | Hugo Herbelin | 2014-10-13 |
* | Documenting option -type-in-type. | Hugo Herbelin | 2014-09-29 |
* | Fixing inversion after having fixed intros_replacing | Hugo Herbelin | 2014-09-10 |
* | Documenting the new Undo semantics | Enrico Tassi | 2014-09-09 |
* | Removing the documentation of the XML plugin. | Pierre-Marie Pédrot | 2014-09-08 |
* | CHANGES: existential variables are always "substituted" in the new tactic eng... | Arnaud Spiwack | 2014-09-08 |
* | CHANGES: Ltac's [refine] accepts [uconstr]. | Arnaud Spiwack | 2014-09-08 |
* | CHANGES: [revgoals]. | Arnaud Spiwack | 2014-09-08 |
* | CHANGES: [Variant], [Set Nonrecursive Elimination Schemes]. | Arnaud Spiwack | 2014-09-08 |
* | CHANGES: binder names from Ltac identifiers. | Arnaud Spiwack | 2014-09-08 |
* | "allows to", like "allowing to", is improper | Jason Gross | 2014-08-25 |
* | Grammar: "allowing to" is not proper English | Jason Gross | 2014-08-25 |
* | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin | 2014-08-18 |
* | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin | 2014-08-05 |
* | Experimentally adding an option for automatically erasing an | Hugo Herbelin | 2014-08-05 |
* | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin | 2014-08-05 |
* | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin | 2014-08-05 |
* | CHANGES: [>…]. | Arnaud Spiwack | 2014-08-01 |
* | CHANGES: [numgoals] and [guard]. | Arnaud Spiwack | 2014-08-01 |
* | Making the error message about bullets more precise. | Pierre Courtieu | 2014-07-31 |