aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/eterm.ml
Commit message (Expand)AuthorAge
* Work with binder lists, problem of tyconsGravatar coq2006-02-21
* Latest fixes, should work fine now for non recursive definitions, although st...Gravatar coq2006-02-21
* Rewrite of the subtac tactic, needs some work on implicit arguments.Gravatar coq2006-02-20
* Changement des named_contextGravatar gregoire2005-12-02
* Subtac: traitement correct des existentielles et de la récursion.Gravatar coq2005-07-15