| Age | Commit message (Expand) | Author |
|---|
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-08-11 | Ensures that let-in's in arities of inductive types work well. Maybe not | herbelin |
| 2009-05-18 | Minor unification changes: | msozeau |
| 2008-12-31 | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin |
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-04-27 | Correction du bug des types singletons pas sous-type de Set | herbelin |
| 2008-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2008-03-09 | Fix a few bugs in Program: use user-given typing constraints for | msozeau |
| 2008-01-31 | Finish let| implementation and document it | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-18 | Nettoyage de code en vue de la release. Plus de Warning: Unused | aspiwack |
| 2007-08-27 | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin |
| 2007-05-23 | Suite restructuration unification et division des problèmes | herbelin |
| 2007-05-11 | Processor integers + Print assumption (see coqdev mailing list for the | aspiwack |
| 2007-03-15 | Suppression argument pattern_source du case_info (code jamais utilisé) | herbelin |
| 2006-10-27 | Ajout fold_rel_declaration et fold_named_declaration | herbelin |
| 2006-08-28 | Export de closedn pour Evarutil | herbelin |
| 2006-05-23 | Ajout substl_named_decl pour mode Maple | herbelin |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-02-16 | added isProd to term.mli. | coq |
| 2006-01-10 | Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-02-12 | Uniformisation de destApplication en destApp; simplification decompose_app | herbelin |
| 2004-11-16 | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot |
| 2004-11-16 | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). | sacerdot |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-11-27 | *** empty log message *** | barras |
| 2003-11-25 | CC: added injection theory | corbinea |
| 2003-06-27 | *** empty log message *** | courant |
| 2003-06-10 | Simplification case_info | herbelin |
| 2003-05-19 | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin |
| 2002-11-18 | Allègement du noyau | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2002-03-04 | Nouveau Rewrite-in plus economique | barras |
| 2002-02-11 | substitution et pattern modulo let | barras |
| 2001-11-20 | Ajout isEvar | herbelin |
| 2001-11-20 | Ajout quelques fonctions; code mort | herbelin |
| 2001-11-12 | Suites modifs du noyau. Univ devient purement fonctionnel. | barras |
| 2001-11-05 | GROS COMMIT: | barras |
| 2001-10-17 | Abstraction de l'immplementation de dirpath et implementation dans l'autre se... | herbelin |
| 2001-10-12 | Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra... | herbelin |
| 2001-10-09 | Suppression des arguments sur les constantes, inductifs et constructeurs | barras |
| 2001-09-19 | Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de... | herbelin |
| 2001-09-10 | Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ... | herbelin |
| 2001-09-09 | Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg... | herbelin |
