aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_command.ml
AgeCommit message (Expand)Author
2006-03-22Subtac fixes, single fixpoint definitions are working again. Added a toggle o...msozeau
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau
2006-03-13Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.msozeau