| Age | Commit message (Expand) | Author |
|---|
| 2009-12-24 | In "simpl c" and "change c with d", c can be a pattern. | herbelin |
| 2009-12-24 | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin |
| 2009-10-23 | First debug... the renaming of librairies was not working and auto/dn were no... | soubiran |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-04-10 | Fix premature optimisation in dependent induction: even variable args need | msozeau |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-06 | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-03-19 | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau |
| 2007-02-13 | Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de | herbelin |
| 2006-06-19 | bug serieux efficacite de ltac | barras |
| 2006-04-27 | - 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-24 | Timide tentative de clarification du statut de l'opérateur de filtrage | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-08 | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin |
| 2005-01-03 | HUGE COMMIT | sacerdot |
| 2004-12-07 | The type Pattern.constr_label was isomorphic to Libnames.global_reference. | sacerdot |
| 2004-11-26 | MAJ PCoFix | herbelin |
| 2004-11-16 | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-12-19 | Substitution dans REvar et PEvar plutot que encodage via noeud application po... | herbelin |
| 2003-09-09 | Ajout construction If primitive dans constr_expr et rawconstr | herbelin |
| 2003-08-11 | Nouvelle mouture du traducteur v7->v8 | herbelin |
| 2003-06-10 | Amélioration afficheur de Cases pour les constr_pattern | herbelin |
| 2003-05-22 | Preservation affichage des ?n en V7 | herbelin |
| 2003-05-21 | Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ... | herbelin |
| 2003-05-19 | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
| 2003-02-01 | Backtrack sur le filtrage des applications partielles (change Tauto/Intuition) | herbelin |
| 2003-01-31 | Ajout d'un filtrage d'application partielle | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-10-01 | Vraie substitutivite de autohints | coq |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2001-11-05 | GROS COMMIT: | barras |
| 2001-10-11 | Suppression option immediate_discharge; nettoyage de Declare et conséquences | herbelin |
| 2001-10-09 | Suppression des arguments sur les constantes, inductifs et constructeurs | barras |
| 2001-09-14 | Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local) | herbelin |
| 2001-05-29 | Facilites pour le debogguage des univers. | coq |
| 2001-03-15 | entetes | filliatr |
| 2001-03-01 | nouvelle implantation de la reduction | barras |
| 2001-02-14 | uniformisation avec constr des lieurs dans rawterm/pattern | herbelin |
| 2001-02-07 | Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref | herbelin |
| 2001-01-03 | Rattrapage d'erreur pour le Case + Eval Compute in pour Definition | delahaye |
| 2000-12-26 | Pattern sera mieux dans Pretyping; relâchement head_pattern_bound | herbelin |
