aboutsummaryrefslogtreecommitdiff
path: root/plugins/interface/xlate.ml
AgeCommit message (Expand)Author
2009-09-20Only one "in" clause in "destruct" even for a multiple "destruct".herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-09-10Added syntax "exists bindings, ..., bindings" for iterated "exists".herbelin
2009-08-14+Fix interface.aspiwack
2009-08-11Infix (r12268 continued)herbelin
2009-08-03Added "etransitivity".herbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-07-24Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"letouzey
2009-06-29Miscellaneous practical commits: herbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey