aboutsummaryrefslogtreecommitdiff
path: root/plugins/decl_mode/decl_proof_instr.ml
AgeCommit message (Expand)Author
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack