aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/g_eterm.ml4
Commit message (Expand)AuthorAge
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* Subtac: traitement correct des existentielles et de la récursion.Gravatar coq2005-07-15