| Commit message (Expand) | Author | Age |
* | - Distinction explicite des parties paramètres et arguments dans le type | herbelin | 2006-04-27 |
* | Standardisation nom option_app en option_map | herbelin | 2006-04-27 |
* | Timide tentative de clarification du statut de l'opérateur de filtrage | herbelin | 2006-04-24 |
* | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
* | Changement des named_context | gregoire | 2005-12-02 |
* | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin | 2005-11-08 |
* | HUGE COMMIT | sacerdot | 2005-01-03 |
* | The type Pattern.constr_label was isomorphic to Libnames.global_reference. | sacerdot | 2004-12-07 |
* | MAJ PCoFix | herbelin | 2004-11-26 |
* | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot | 2004-11-16 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Substitution dans REvar et PEvar plutot que encodage via noeud application po... | herbelin | 2003-12-19 |
* | Ajout construction If primitive dans constr_expr et rawconstr | herbelin | 2003-09-09 |
* | Nouvelle mouture du traducteur v7->v8 | herbelin | 2003-08-11 |
* | Amélioration afficheur de Cases pour les constr_pattern | herbelin | 2003-06-10 |
* | Preservation affichage des ?n en V7 | herbelin | 2003-05-22 |
* | Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ... | herbelin | 2003-05-21 |
* | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin | 2003-05-19 |
* | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin | 2003-04-07 |
* | Backtrack sur le filtrage des applications partielles (change Tauto/Intuition) | herbelin | 2003-02-01 |
* | Ajout d'un filtrage d'application partielle | herbelin | 2003-01-31 |
* | Réforme de l'interprétation des termes : | herbelin | 2002-11-14 |
* | Vraie substitutivite de autohints | coq | 2002-10-01 |
* | Modules dans COQ\!\!\!\! | coq | 2002-08-02 |
* | GROS COMMIT: | barras | 2001-11-05 |
* | Suppression option immediate_discharge; nettoyage de Declare et conséquences | herbelin | 2001-10-11 |
* | Suppression des arguments sur les constantes, inductifs et constructeurs | barras | 2001-10-09 |
* | Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local) | herbelin | 2001-09-14 |
* | Facilites pour le debogguage des univers. | coq | 2001-05-29 |
* | entetes | filliatr | 2001-03-15 |
* | nouvelle implantation de la reduction | barras | 2001-03-01 |
* | uniformisation avec constr des lieurs dans rawterm/pattern | herbelin | 2001-02-14 |
* | Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref | herbelin | 2001-02-07 |
* | Rattrapage d'erreur pour le Case + Eval Compute in pour Definition | delahaye | 2001-01-03 |
* | Pattern sera mieux dans Pretyping; relâchement head_pattern_bound | herbelin | 2000-12-26 |