aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/decl_mode/ppdecl_proof.ml
Commit message (Expand)AuthorAge
* Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* rewiring Czar printers that were disabledGravatar Pierre Corbineau2015-03-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22