index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
g_basevernac.ml4
Commit message (
Expand
)
Author
Age
*
Renaming Print Canonical Structure into Print Canonical Projections
herbelin
2005-02-18
*
Ajout Print Canonical Structures
herbelin
2005-02-12
*
New command "Print Rewrite HindDb dbname".
sacerdot
2004-11-17
*
Ajout 'Locate Module'
herbelin
2004-11-17
*
Nouvelle en-tête
herbelin
2004-07-16
*
Bug syntaxe AddPath
herbelin
2004-05-14
*
Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...
herbelin
2004-01-29
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
Ajout Print Implicit avec depliage du type
herbelin
2003-11-15
*
Suppression SearchNamed finalement redondant avec SearchAbout
herbelin
2003-11-10
*
Heritage des notations v7 seulement si zero information v8
herbelin
2003-11-01
*
Ajout de Print Visibility
herbelin
2003-10-28
*
Independance de grammar.cmo vis a vis de Search
herbelin
2003-10-23
*
Integration de SearchNamed dans SearchAbout
herbelin
2003-10-22
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Ajout d'une fonction de recherche sur les composantes du nom des objets
herbelin
2003-10-13
*
Implantation de l'option 'format' des Notations
herbelin
2003-10-01
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Ajout 'About'
herbelin
2003-09-26
*
Re-possibilite changement chaine infixe en passant v7 a v8
herbelin
2003-09-26
*
Distfix aussi adopte le nouveau schema de V8only
herbelin
2003-09-22
*
Changement de la politique de V8only: V8only tout seul signifie
herbelin
2003-09-21
*
Mise en place des V8Notation et V8Infix pour déclarer des notations en
herbelin
2003-09-19
*
Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...
herbelin
2003-09-12
*
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
*
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-29
*
Ajout "at next level" dans Notation
herbelin
2003-04-17
*
Ajout option 'Local' à Infix et Notation
herbelin
2003-04-11
*
Ajout option "Local" à "Open Scope"
herbelin
2003-04-08
*
*** empty log message ***
barras
2003-03-21
*
*** empty log message ***
barras
2003-03-12
*
SearchAbout
filliatr
2003-01-06
*
Meilleure factorisation des entrées NEXT internes
herbelin
2002-12-15
*
Raffinement syntaxe Infix
herbelin
2002-11-29
*
Oubli
herbelin
2002-11-28
*
Correction sur commit précédent
herbelin
2002-11-27
*
MAJ delimiters et niveaux d'associativite
herbelin
2002-11-25
*
Retour sur le choix des delimiteurs
herbelin
2002-11-25
*
Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...
herbelin
2002-11-24
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
fix forbidden currified constructors
ddr
2002-11-07
*
Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...
herbelin
2002-10-22
*
Prise en compte des délimiteurs dans les motifs de Cases
herbelin
2002-10-21
*
Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une
herbelin
2002-10-14
*
Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...
herbelin
2002-10-13
*
Pretty-printing preliminaire des modules, commandes
coq
2002-08-19
*
Pour assurer une compatibilite avec la 7.3
herbelin
2002-07-15
[next]