aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacintern.ml
AgeCommit message (Expand)Author
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-11-25Monomorphization (tactics)ppedrot
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey