aboutsummaryrefslogtreecommitdiff
path: root/contrib/firstorder
AgeCommit message (Expand)Author
2009-02-06pushed evar reduction in kernelbarras
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-10-26Fixes and refinements regarding occurrence selection:herbelin
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2008-04-16first-order --> firstorder (kills a warning about not being a valid id)letouzey