| Commit message (Expand) | Author | Age |
... | |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
* | Monomorphization (kernel) | ppedrot | 2012-11-22 |
* | 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-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Completing r14448 and thus continuing r14407 (using Cast to propagate | herbelin | 2011-09-24 |
* | Having added a special Cast for remembering the use of conversion | herbelin | 2011-09-04 |
* | Propagated information from the reduction tactics to the kernel so | herbelin | 2011-08-10 |
* | Term_typing, Typeops: replace some generic '=' on constr by eq_constr | puech | 2011-07-29 |
* | Revert "Add [Polymorphic] flag for defs" | msozeau | 2011-04-13 |
* | Add [Polymorphic] flag for defs | msozeau | 2011-04-13 |
* | Replaced printing number of ill-typed branch by printing name of constructor | herbelin | 2011-04-08 |
* | Univ.constraints made fully abstract instead of being a Set of abstract stuff | letouzey | 2010-12-18 |
* | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Réutilisation de l'infrastructure pour le polymorphisme d'univers des | herbelin | 2008-04-30 |
* | Correction du bug des types singletons pas sous-type de Set | herbelin | 2008-04-27 |
* | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin | 2007-08-27 |
* | Compatibilité du polymorphisme de constantes avec les sections. | herbelin | 2006-10-29 |
* | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin | 2006-10-28 |
* | Déplacement de on_judgment_type de Typeops vers Termops | herbelin | 2006-10-06 |
* | - Indtypes: en attente opinion CoRN, les occurrences de Type non explicites | herbelin | 2006-05-28 |
* | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin | 2006-05-23 |
* | Inductifs avec polymorphisme de sorte (version initiale) | herbelin | 2006-03-29 |
* | Orthographe de 'instantiate' | herbelin | 2005-12-17 |
* | Changement des named_context | gregoire | 2005-12-02 |
* | Nettoyage suite nouveaux avertissements Y et Z de ocaml 3.09 | herbelin | 2005-11-08 |
* | Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed | sacerdot | 2005-01-14 |
* | COMMITED BYTECODE COMPILER | barras | 2004-10-20 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Suppression StronglyClassical, StronglyConstructive devient plus concretement... | herbelin | 2003-11-08 |
* | Set devient predicatif par defaut | herbelin | 2003-10-28 |
* | Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse la | herbelin | 2002-12-10 |
* | Déplacement du hash-consing vers declare.ml | herbelin | 2002-12-10 |
* | Renoncement | herbelin | 2002-08-13 |
* | Modules dans COQ\!\!\!\! | coq | 2002-08-02 |
* | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin | 2002-05-29 |
* | petite erreur dans le typage des let-in | barras | 2002-03-28 |
* | petit nettoyage de kernel/inductive | barras | 2002-02-07 |
* | compat ocaml 3.03 | filliatr | 2001-12-13 |
* | types vs constr | herbelin | 2001-11-20 |
* | Suites modifs du noyau. Univ devient purement fonctionnel. | barras | 2001-11-12 |
* | Rétablissement de la persistance des Cast; typage des LetIn sans recours à ... | herbelin | 2001-11-08 |
* | GROS COMMIT: | barras | 2001-11-05 |
* | Suppression des arguments sur les constantes, inductifs et constructeurs | barras | 2001-10-09 |