aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/smartlocate.ml
Commit message (Expand)AuthorAge
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* Fixed a bug when reporting unexisting reference to an inductiveGravatar herbelin2009-10-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11