aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/quote/quote.ml
Commit message (Expand)AuthorAge
...
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Add a more general quote constructionGravatar glondu2009-03-30
* Fix some typos and spacesGravatar glondu2009-03-30
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20