aboutsummaryrefslogtreecommitdiff
path: root/pretyping/classops.ml
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Goptions do not rely anymore on generic equality.Pierre-Marie Pédrot
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2014-01-27Abstracting away coercion indexes in Classops.Pierre-Marie Pédrot
2014-01-26Coercions: avoid imperative data structureEnrico Tassi
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-08-03Small fixes due to the arrival of OCaml 3.12.ppedrot
2013-05-14Removing Gmap from Classops. Fold order only mattered for printing.ppedrot
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-02-19Classops : avoid some use of Gmapletouzey
2012-12-14Modulification of identifierppedrot
2012-11-25More equality functionsppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-01Cleaning Pp.ppnl useppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-12-07Fixing a bug of commit r13310 (activating coercions only when moduleherbelin
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-07-29Classops: generic equality on constr replaced by eq_constrpuech
2011-02-11An automatic substitution of scope at functor applicationletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-23Some fine-tuning after removal of automatic imports of coercions in r13310herbelin
2010-07-22Made coercions active only when modules are imported.herbelin
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-04-08Some dead code removal + cleanupsletouzey
2009-02-06pushed evar reduction in kernelbarras
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 21:02:14 +0000