aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/ccalgo.ml
Commit message (Expand)AuthorAge
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\
| * Fixing a source of inefficiency and an artificial dependency in theGravatar Daniel de Rauglaudre2016-04-08
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Univs: fix an evar leak in congruenceGravatar Matthieu Sozeau2015-10-02
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Getting rid of generic hashes in cc plugin.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Avoid polymorphic comparison (plugins/cc).Gravatar xclerc2013-10-14
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Tentative fix for #3054: we refresh universes in a term generatedGravatar ppedrot2013-07-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Restrict (try...with...) to avoid catching critical exn (part 9)Gravatar letouzey2013-03-13
* Fixed synchronicity of filter with evar context in new_goal_with.Gravatar herbelin2013-01-29
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Array.create is deprecatedGravatar pboutill2012-12-19
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* Noise for nothingGravatar pboutill2012-03-02
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* 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
* commit 13400 and 13409.Gravatar soubiran2010-09-13
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20