| Age | Commit message (Expand) | Author |
|---|
| 2006-01-11 | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin |
| 2006-01-09 | Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement... | herbelin |
| 2006-01-08 | Prise en compte, enfin, du contexte des types de retour de ACases et RCases | herbelin |
| 2006-01-08 | Prise en compte de notations numérales définies au niveau utilisateur + tra... | herbelin |
| 2006-01-08 | Enregistrement dans glob.dump des utilisations de notations numériques (qui ... | herbelin |
| 2006-01-08 | Automatisation de l'utilisation de token primitifs dans les motifs de filtrag... | herbelin |
| 2006-01-08 | Ajout rawconstr_of_aconstr | herbelin |
| 2006-01-05 | Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ... | herbelin |
| 2006-01-04 | Suppression des coercions non seulement avant l'affichage des notations mais ... | herbelin |
| 2006-01-03 | Redéclaration de la notation à l'import pour être cohérent avec l'activat... | herbelin |
| 2005-12-30 | Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de... | herbelin |
| 2005-12-30 | Ajout booléens; nettoyage | herbelin |
| 2005-12-26 | Petite correction nom QuantHypArgType suite suppression traducteur | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-23 | Simplifification de vernac_expr li l'abandon du traducteur | herbelin |
| 2005-12-22 | Correction bugs commit précédent | herbelin |
| 2005-12-21 | Restructuration des points d'entrée de Pretyping et Constrintern | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-21 | Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05) | herbelin |
| 2005-11-19 | Correction de la correction du test sur le nombre de parametres d'une projection | herbelin |
| 2005-11-08 | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin |
| 2005-11-02 | Types inductifs parametriques | mohring |
| 2005-09-09 | Conséquences nettoyage pretyping.ml | herbelin |
| 2005-06-03 | Prise en compte de l'utilisation des notations récursives pour faire une not... | herbelin |
| 2005-05-20 | Adoption du nom canonique global_of_constr pour éviter confusion avec type r... | herbelin |
| 2005-05-20 | Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve... | herbelin |
| 2005-05-17 | Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux... | herbelin |
| 2005-02-18 | Moving centralised discharge into dispatched discharge_function; required to ... | herbelin |
| 2005-02-18 | Standardisation of function names about global references (especially, renami... | herbelin |
| 2005-02-07 | Bug affichage rawconstr | herbelin |
| 2005-02-06 | Nettoyage et documentation de Library | herbelin |
| 2005-01-21 | Pour cible make doc | herbelin |
| 2005-01-21 | Compatibilité ocamlweb pour cible doc | herbelin |
| 2005-01-13 | Construct "T with (Definition|Module) id := c" generalized to | sacerdot |
| 2005-01-03 | HUGE COMMIT | sacerdot |
| 2005-01-03 | Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p... | herbelin |
| 2005-01-02 | Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p... | herbelin |
| 2004-12-25 | Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque... | herbelin |
| 2004-12-24 | Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque... | herbelin |
| 2004-12-22 | Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem... | herbelin |
| 2004-12-09 | Restauration type casted_open_constr pour tactique refine car l'unification n... | herbelin |
| 2004-12-06 | Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti... | herbelin |
| 2004-11-17 | Message d'erreur | herbelin |
| 2004-11-17 | Suppression capture des variables par lieurs non liés dans Notation; simplif... | herbelin |
| 2004-11-17 | Suppression capture des variables par lieurs non liés dans Notation | 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-09-15 | hiding the meta_map in evar_defs | barras |
| 2004-09-09 | Ajout de or-pattern pour le match-with v8 | herbelin |
| 2004-08-23 | Interpretation et affichage corrects des notations LetTuple, affichage des no... | herbelin |
