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