aboutsummaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_command.ml
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11- Resolve type class constraints before trying to find unresolvedmsozeau
2009-06-17Fallback on not using [fix_proto] if the right imports aren't there, the msozeau
2009-04-28More efficient handling of evars in Program Fixpoint commands.msozeau
2009-04-24Backporting 12080 (fixing bug #2091 on bad rollback in the "where"herbelin
2009-04-24- New cleaning phase for the entry points of pretyping.mlherbelin
2009-04-08Experimental support for automatic destruction of recursive calls andmsozeau
2009-04-08Fix bug #2083 for good: verify that the measure and relation aremsozeau
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-03-26Fixes in Program well-founded definitions:msozeau
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey