aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/interp.ml
Commit message (Expand)AuthorAge
* Work on recursive definitionsGravatar coq2006-02-22
* 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
* Fix minor bugGravatar coq2006-02-20
* Monday work, working with coercions and implicit argsGravatar coq2006-02-20
* Rewrite of the subtac tactic, needs some work on implicit arguments.Gravatar coq2006-02-20