aboutsummaryrefslogtreecommitdiff
path: root/plugins/decl_mode/ppdecl_proof.ml
AgeCommit message (Expand)Author
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack