aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/test/measure.v
Commit message (Expand)AuthorAge
* Backport code from command.ml to subtac_command.ml for defininingGravatar msozeau2008-02-08
* Mutually structurally recursive defs and rec using measures added.Gravatar msozeau2006-06-22