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