aboutsummaryrefslogtreecommitdiff
path: root/interp/smartlocate.ml
AgeCommit message (Expand)Author
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Noise for nothingpboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
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