| Commit message (Expand) | Author | Age |
... | |
* | - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing | herbelin | 2009-04-08 |
* | - Structuring Numbers and fixing Setoid in stdlib's doc. | herbelin | 2009-01-19 |
* | Fixing/improving management of uniform prefix Local and Global | herbelin | 2009-01-14 |
* | More factorization of inductive/record and typeclasses: move class | msozeau | 2008-11-09 |
* | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin | 2008-10-19 |
* | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
* | Correction d'un autre bug autour de la gestion des niveaux vides de | herbelin | 2008-07-11 |
* | Résolution bug #1850 sur notations avec niveaux inconnus de | herbelin | 2008-05-26 |
* | - Cleanup parsing of binders, reducing to a single production for all | msozeau | 2008-05-11 |
* | ** Efficacité, bugs, robustesse CoqIDE ** | herbelin | 2008-05-08 |
* | Contournement laborieux de la "feature" de camlp5 qui entrainait le | herbelin | 2008-04-30 |
* | Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour | herbelin | 2008-04-26 |
* | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau | 2008-03-06 |
* | Generalize instance declarations to any context, better name handling. Add ho... | msozeau | 2008-01-15 |
* | Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp... | msozeau | 2008-01-07 |
* | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
* | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack | 2007-12-06 |
* | Factorisation des opérations sur le type option de Util dans un module | aspiwack | 2007-12-05 |
* | Creation of a new token PATTERNIDENT (?ident) for intro patterns, so | glondu | 2007-09-28 |
* | * Adding compability with ocaml 3.10 + camlp5 (rework of | letouzey | 2007-09-15 |
* | Generalized CAMLP4USE for pp dependencies | corbinea | 2007-07-16 |
* | Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a | herbelin | 2007-04-11 |
* | Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5 | herbelin | 2007-04-10 |
* | gestion speciale du niveau 5 des ltac | barras | 2006-11-02 |
* | Declarative Proof Language: main commit | corbinea | 2006-09-20 |
* | Correction incohérence parsing de %delim dans les motifs | herbelin | 2006-07-12 |
* | Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ... | herbelin | 2006-07-04 |
* | Mise à jour (avec retard) des niveaux de la table default_pattern_levels | herbelin | 2006-07-03 |
* | Changement du type d'argument 'TacticArgType X' en un type | herbelin | 2006-06-08 |
* | Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement... | herbelin | 2006-01-09 |
* | Mini-restructuration | herbelin | 2005-12-30 |
* | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
* | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin | 2005-11-08 |
* | Added entry constr_may_eval for tactic extensions (new syntax) | herbelin | 2005-06-22 |
* | Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux... | herbelin | 2005-05-17 |
* | Construct "T with (Definition|Module) id := c" generalized to | sacerdot | 2005-01-13 |
* | Restauration type casted_open_constr pour tactique refine car l'unification n... | herbelin | 2004-12-09 |
* | Uniformisation du nom d'entrée openconstr en le nom du type open_constr | herbelin | 2004-12-06 |
* | Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti... | herbelin | 2004-12-06 |
* | Bug mauvais nom d'entrée binder_constr quand récursion gauche | herbelin | 2004-10-27 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Mise en place de motifs récursifs dans Notation; quelques simplifications au... | herbelin | 2004-03-17 |
* | Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no... | herbelin | 2004-03-02 |
* | Généralisation du type ltac Identifier en IntroPattern; prise en compte des... | herbelin | 2004-03-01 |
* | Ajout de lconstr, constr et binder_constr dans Print Grammar constr | herbelin | 2004-02-17 |
* | Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p... | herbelin | 2003-12-04 |
* | Nouvelle tactique EExists | clrenard | 2003-12-01 |
* | Ajout ne_string | herbelin | 2003-11-27 |
* | Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons... | herbelin | 2003-11-20 |
* | Protection contre l'effacement des niveaux vides de operconstr et pattern par... | herbelin | 2003-11-19 |