aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc/ccalgo.ml
AgeCommit message (Expand)Author
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-08Fixing a source of inefficiency and an artificial dependency in theDaniel de Rauglaudre
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-10-02Univs: fix an evar leak in congruenceMatthieu Sozeau
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-03Getting rid of generic hashes in cc plugin.Pierre-Marie Pédrot
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2013-10-14Avoid polymorphic comparison (plugins/cc).xclerc
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-07-29Tentative fix for #3054: we refresh universes in a term generatedppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
2013-01-29Fixed synchronicity of filter with evar context in new_goal_with.herbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-19Array.create is deprecatedpboutill
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-26Cleaning, renaming obscure functions and documenting in Hashcons.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30Getting rid of Pp.msgppedrot
2012-03-02Noise for nothingpboutill
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-07-29Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...puech
2011-07-29Ccproof: generic equality on term replaced by term_equalpuech
2010-09-13commit 13400 and 13409.soubiran
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-02Improved parameterization of Coq:herbelin
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:24:44 +0000