index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
g_prim.ml4
Commit message (
Expand
)
Author
Age
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Generalized the possibility to refer to a global name by a notation
herbelin
2009-09-11
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
The lexer is changer to break former PATTERNIDENT into two tokens.
amahboub
2008-10-30
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Bug résiduel du backtrack de coqide se produisant lorsque la limite de
herbelin
2008-07-10
*
Creation of a new token PATTERNIDENT (?ident) for intro patterns, so
glondu
2007-09-28
*
Generalized CAMLP4USE for pp dependencies
corbinea
2007-07-16
*
Oubli lors suppression traducteur
herbelin
2006-01-23
*
Autres suppressions de composantes du traducteur
herbelin
2005-12-27
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-24
*
Suppression quotify
herbelin
2004-07-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...
herbelin
2004-03-02
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
*** empty log message ***
barras
2003-03-12
*
Ajout d'une entre Prim.bigint
herbelin
2002-11-28
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
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
*
Correction mauvais ordre dans le parsing des dirpath; MAJ de la quotification
herbelin
2002-06-05
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
GROS COMMIT:
barras
2001-11-05
*
bug incompatibilité
herbelin
2001-08-13
*
Parsing
herbelin
2001-08-10
*
Changement de la structure des points fixes
barras
2001-05-03
*
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...
filliatr
2001-04-04
*
entetes
filliatr
2001-03-15
*
Nouveau lexeme METAIDENT pour les $id
herbelin
2000-11-20
*
Changement/extension dans les noms de parseurs de Grammar
herbelin
2000-11-07
*
compilation des fichiers ml4 sans GNUseries
filliatr
2000-11-03
*
Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...
herbelin
2000-10-18
*
Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...
herbelin
2000-07-28
*
compilation des grammaires (ouf)
filliatr
1999-09-08
*
modules grammaire Coq
filliatr
1999-09-08