aboutsummaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_pretyping.mli
AgeCommit message (Expand)Author
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-03-14Second step of integration of Program:msozeau
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