| Commit message (Expand) | Author | Age |
* | Getting rid of Pp.msgnl and Pp.message. | ppedrot | 2012-06-01 |
* | remove many excessive open Util & Errors in mli's | letouzey | 2012-05-29 |
* | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey | 2012-05-29 |
* | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey | 2012-05-29 |
* | Slight change in the semantics of arguments scopes: scopes can no | herbelin | 2012-03-26 |
* | Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic | herbelin | 2012-03-20 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Simplified the way internalization_data (i.e. bindings of bound vars | herbelin | 2010-07-22 |
* | New script dev/tools/change-header to automatically update Coq files headers. | herbelin | 2010-06-22 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill | 2010-04-29 |
* | Several bug-fixes and improvements of coqdoc | herbelin | 2010-03-29 |
* | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | - Addition of "Reserved Infix" continued. | herbelin | 2009-09-14 |
* | Generalized the possibility to refer to a global name by a notation | herbelin | 2009-09-11 |
* | Add support for "Infix ... := constr" instead of just "Infix ... := ref". | herbelin | 2009-08-11 |
* | - Cleaning (unification of ML names, removal of obsolete code, | herbelin | 2009-04-27 |
* | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin | 2008-10-19 |
* | Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ) | herbelin | 2007-02-24 |
* | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
* | Simplifification de vernac_expr li l'abandon du traducteur | herbelin | 2005-12-23 |
* | Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux... | herbelin | 2005-05-17 |
* | Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p... | herbelin | 2005-01-02 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Traitement plus clair, notamment pour Locate, de quand quoter les composantes... | herbelin | 2003-11-22 |
* | Changement 'as notation' en 'where notation' | herbelin | 2003-10-14 |
* | Implantation de l'option 'format' des Notations | herbelin | 2003-10-01 |
* | Ajout 'Close Scope'. | herbelin | 2003-09-30 |
* | parsing | herbelin | 2003-09-19 |
* | Ajout 'Print Scopes' et 'Bind Scope with classes' | herbelin | 2003-09-12 |
* | Traduction de Distfix | herbelin | 2003-09-10 |
* | Ajout V8Notation | herbelin | 2003-05-22 |
* | Prise en compte des syntaxes v8 dans Uninterpreted Notation | herbelin | 2003-04-29 |
* | Ajout "at next level" dans Notation | herbelin | 2003-04-17 |
* | Ajout option 'Local' à Infix et Notation | herbelin | 2003-04-11 |
* | *** empty log message *** | barras | 2003-03-12 |
* | Raffinement syntaxe Infix | herbelin | 2002-11-29 |
* | MAJ delimiters et niveaux d'associativite | herbelin | 2002-11-25 |
* | Réforme de l'interprétation des termes : | herbelin | 2002-11-14 |
* | Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;... | herbelin | 2002-10-22 |
* | Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha... | herbelin | 2002-10-13 |
* | Modules dans COQ\!\!\!\! | coq | 2002-08-02 |
* | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin | 2002-05-29 |
* | entetes | filliatr | 2001-03-15 |
* | protection contre certaines exceptions levees par marshal_{in,out} | barras | 2001-03-09 |
* | Déplacement de qualid dans Nametab, hors du noyau | herbelin | 2001-03-01 |
* | syntaxe AST Inversion + commentaires ocamlweb autour de $ | filliatr | 2000-12-12 |
* | Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's... | herbelin | 2000-11-22 |