aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_utils.ml
AgeCommit message (Expand)Author
2006-06-20Rewrite of the recursive defs handling in progress.msozeau
2006-06-01Fix some nasty bug with the evars-to-dependent sum encoding.msozeau
2006-05-29The "clean integration of subtac" patch.msozeau
2006-04-10Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...msozeau
2006-04-07- Documentation of the Program tactics.msozeau
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau