aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/ccproof.ml
Commit message (Expand)AuthorAge
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Fixing a source of inefficiency and an artificial dependency in theGravatar Daniel de Rauglaudre2016-04-08
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
* Revert "Fixing a loop in proof reconstruction for congruence (#2447)."Gravatar Hugo Herbelin2014-10-17
* Fixing a loop in proof reconstruction for congruence (#2447).Gravatar Hugo Herbelin2014-10-17
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* 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
* Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...Gravatar puech2011-07-29
* Ccproof: generic equality on term replaced by term_equalGravatar puech2011-07-29
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20