aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Mention guard condition in CHANGES.Gravatar Maxime Dénès2015-01-15
* CHANGES: my recent updates to Ltac.Gravatar Arnaud Spiwack2015-01-14
* More in CHANGES about local definitionsGravatar Pierre-Marie Pédrot2015-01-13
* CHANGES: mention "Optimize (Heap|Proof)"Gravatar Enrico Tassi2015-01-10
* Update + English in CHANGESGravatar Hugo Herbelin2015-01-08
* Start credits for 8.5.Gravatar Matthieu Sozeau2015-01-08
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Document native_compute.Gravatar Maxime Dénès2015-01-08
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* Document the new behavior of lazymatch.Gravatar Guillaume Melquiond2014-12-30
* more CHANGESGravatar Enrico Tassi2014-12-30
* Minor modification of CHANGE.Gravatar Pierre Courtieu2014-12-23
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* In CHANGES, alerting about stronger check on notation level modifiers.Gravatar Hugo Herbelin2014-12-16
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* Documenting the Set Refine Instance Mode.Gravatar Pierre-Marie Pédrot2014-11-30
* Hopefully the last word on having "simpl f" complying with theGravatar Hugo Herbelin2014-11-18
* Fixing detection of occurrences in the presence of nested subterms forGravatar Hugo Herbelin2014-11-18
* Documenting use of colors in Coq.Gravatar Pierre-Marie Pédrot2014-11-17
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Updating CHANGES (evars as ident).Gravatar Hugo Herbelin2014-11-11
* American spelling + layout in CHANGES.Gravatar Hugo Herbelin2014-11-11
* Fixing careless name confusion in CHANGES.Gravatar Pierre-Marie Pédrot2014-11-04
* Documenting the change of semantics of the replace tactic.Gravatar Pierre-Marie Pédrot2014-11-04
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Documenting some incompatibilities in (non) Import of ML tactics,Gravatar Hugo Herbelin2014-10-24
* Addressing report #3279 (inconsistency of behavior of the -> and <-Gravatar Hugo Herbelin2014-10-24
* CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defin...Gravatar Arnaud Spiwack2014-10-22
* Mentioning incompatibility shown in #3718 and coming from #3050Gravatar Hugo Herbelin2014-10-13
* Documenting option -type-in-type.Gravatar Hugo Herbelin2014-09-29
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
* Documenting the new Undo semanticsGravatar Enrico Tassi2014-09-09
* Removing the documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* CHANGES: existential variables are always "substituted" in the new tactic eng...Gravatar Arnaud Spiwack2014-09-08
* CHANGES: Ltac's [refine] accepts [uconstr].Gravatar Arnaud Spiwack2014-09-08
* CHANGES: [revgoals].Gravatar Arnaud Spiwack2014-09-08
* CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].Gravatar Arnaud Spiwack2014-09-08
* CHANGES: binder names from Ltac identifiers.Gravatar Arnaud Spiwack2014-09-08
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* CHANGES: [>…].Gravatar Arnaud Spiwack2014-08-01
* CHANGES: [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
* Making the error message about bullets more precise.Gravatar Pierre Courtieu2014-07-31