aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/smartlocate.ml
Commit message (Expand)AuthorAge
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* 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