aboutsummaryrefslogtreecommitdiff
path: root/toplevel/class.ml
AgeCommit message (Expand)Author
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-10-18declaration_hooks use Ephemerongareuselesinge
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of identifierppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
2012-04-05Relax uniform inheritance conditiongareuselesinge
2012-03-02Noise for nothingpboutill
2011-12-12Proof using ...gareuselesinge
2011-07-29Class: generic equality on constr replaced by destructorspuech
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-02-11An automatic substitution of scope at functor applicationletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-12Applying François' patch fixing grammar of uniform inheritance condition mes...herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-08Some dead code removal + cleanupsletouzey
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
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-06-10- Correction bug 1841 (identificateurs incorrects avec Subclass)herbelin
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
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
2005-12-02Changement des named_contextgregoire
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2004-11-29Complétion commit précédentherbelin
2004-11-26Réduire pour trouver l'arité d'une classeherbelin
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-11-12Changement dans les boxed values .gregoire
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 15:07:16 +0000