aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/class.ml
Commit message (Expand)AuthorAge
* Fix bug #3453, not recognizing primitive projections in Coercion declarations.Gravatar Matthieu Sozeau2014-07-29
* Adapt coercion code to work with projections as target classes.Gravatar Matthieu Sozeau2014-06-17
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (toplevel)Gravatar ppedrot2012-11-26
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* 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
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
* Relax uniform inheritance conditionGravatar gareuselesinge2012-04-05
* Noise for nothingGravatar pboutill2012-03-02
* Proof using ...Gravatar gareuselesinge2011-12-12
* Class: generic equality on constr replaced by destructorsGravatar puech2011-07-29
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* An automatic substitution of scope at functor applicationGravatar letouzey2011-02-11
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Applying François' patch fixing grammar of uniform inheritance condition mes...Gravatar herbelin2010-06-12
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Correction bug 1841 (identificateurs incorrects avec Subclass)Gravatar herbelin2008-06-10
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08