| Age | Commit message (Expand) | Author |
|---|
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Fix interface for template polymorphism, cleaning up code in all typing algor... | Matthieu Sozeau |
| 2014-05-06 | Properly reinstate old-style polymorphism in the kernel and pretyping/retyping. | Matthieu Sozeau |
| 2014-05-06 | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-10 | Useless Array.to_list in Typeops. | Pierre-Marie Pédrot |
| 2013-12-30 | Support for evars and metas in native compiler. | Maxime Dénès |
| 2013-05-14 | Delayed the computation of parameters in sort polymorphism of | herbelin |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-02-28 | More informative error when a global reference is used in a context of | herbelin |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-11-22 | Monomorphization (kernel) | ppedrot |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-09-24 | Completing r14448 and thus continuing r14407 (using Cast to propagate | herbelin |
| 2011-09-04 | Having added a special Cast for remembering the use of conversion | herbelin |
| 2011-08-10 | Propagated information from the reduction tactics to the kernel so | herbelin |
| 2011-07-29 | Term_typing, Typeops: replace some generic '=' on constr by eq_constr | puech |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-04-08 | Replaced printing number of ill-typed branch by printing name of constructor | herbelin |
| 2010-12-18 | Univ.constraints made fully abstract instead of being a Set of abstract stuff | letouzey |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2008-04-30 | Réutilisation de l'infrastructure pour le polymorphisme d'univers des | herbelin |
| 2008-04-27 | Correction du bug des types singletons pas sous-type de Set | herbelin |
| 2007-08-27 | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin |
| 2006-10-29 | Compatibilité du polymorphisme de constantes avec les sections. | herbelin |
| 2006-10-28 | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin |
| 2006-10-06 | Déplacement de on_judgment_type de Typeops vers Termops | herbelin |
| 2006-05-28 | - Indtypes: en attente opinion CoRN, les occurrences de Type non explicites | herbelin |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-03-29 | Inductifs avec polymorphisme de sorte (version initiale) | herbelin |
| 2005-12-17 | Orthographe de 'instantiate' | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-08 | Nettoyage suite nouveaux avertissements Y et Z de ocaml 3.09 | herbelin |
| 2005-01-14 | Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed | sacerdot |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-11-08 | Suppression StronglyClassical, StronglyConstructive devient plus concretement... | herbelin |
| 2003-10-28 | Set devient predicatif par defaut | herbelin |
| 2002-12-10 | Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse la | herbelin |
