aboutsummaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_pretyping.mli
AgeCommit message (Expand)Author
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-07-27Minor fixes:msozeau
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-05-16Support for definition hooks in subtac.msozeau
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey