aboutsummaryrefslogtreecommitdiff
path: root/interp/smartlocate.ml
AgeCommit message (Expand)Author
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-10-28Fixed a bug when reporting unexisting reference to an inductiveherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin