aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pattern.mli
AgeCommit message (Expand)Author
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2000-12-26Pattern sera mieux dans Pretyping; relâchement head_pattern_boundherbelin