aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppconstr.ml
Commit message (Expand)AuthorAge
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...Gravatar herbelin2004-12-29
* Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...Gravatar herbelin2004-12-25
* Univ.pr_univ ==> Univ.pr_uniGravatar sacerdot2004-11-04
* Affichage des universGravatar herbelin2004-11-04
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* Ajout de or-pattern pour le match-with v8Gravatar herbelin2004-09-09
* Précisions message d'erreurGravatar herbelin2004-08-23
* Nouvelle en-têteGravatar herbelin2004-07-16
* Mise en place de motifs récursifs dans Notation; quelques simplifications au...Gravatar herbelin2004-03-17
* modif des fixpoints pour que si on donne une notation au produit, les pts fix...Gravatar barras2004-03-05
* Keep structure information for Fixpoint declaration and Fix termsGravatar bertot2004-02-26
* reparation bug moins unaire (erreur de PP)Gravatar barras2003-11-18
* Extensibilite de la grammaires des patternsGravatar herbelin2003-11-01
* Mise en place d'implicites par noms en v8Gravatar herbelin2003-09-21
* Ajout construction If primitive dans constr_expr et rawconstrGravatar herbelin2003-09-09
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Retour vieil afficheurGravatar herbelin2003-03-03
* Retour nouvel afficheurGravatar herbelin2003-02-27
* Rétablissement pr_patternGravatar herbelin2003-01-19
* Retour printer ast pour V7.4Gravatar herbelin2003-01-07
* Affinement affichageGravatar herbelin2002-12-21
* Quelques bugs d'affichage; mise en place du nouveau printer de vieille syntaxeGravatar herbelin2002-12-15
* Bugs diversGravatar herbelin2002-12-10
* Problèmes et améliorations affichage; Changement SimplGravatar herbelin2002-12-09
* Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...Gravatar herbelin2002-12-04
* bugs d'affichage (confusion key/scope dans les délimiteurs)Gravatar herbelin2002-12-03
* Re-déplacement du résultat de Grammar au niveau constr_exprGravatar herbelin2002-12-02
* Réaffichage des Syntactic Definition (printer constr_expr).Gravatar herbelin2002-11-26
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...Gravatar herbelin2002-11-24
* Passage à une représentation des fixpoints plus primitive dans constr_expr ...Gravatar herbelin2002-11-15
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* passage a ocaml 3.06Gravatar herbelin2002-09-27
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Finalement un seul constr pour l'instant dans ExtraRedExprGravatar herbelin2002-05-30
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29