index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
translate
/
ppconstrnew.mli
Age
Commit message (
Expand
)
Author
2005-12-26
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-01-21
Compatibilité ocamlweb pour cible doc
herbelin
2004-07-16
Nouvelle en-tête
herbelin
2004-03-05
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-01-05
certains id n'etaient pas renommes pour eviter les conflits avec les mots-cles
barras
2004-01-02
meilleure presentation des commentaires du traducteur
barras
2003-11-12
Mise en place systeme de renommage des noms de variables liees dans la biblio...
herbelin
2003-10-21
Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par...
herbelin
2003-10-10
Ajout printers pour constr et constr_pattern (sans traduction)
herbelin
2003-09-22
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-16
Pour appliquer les noms reserves aussi aux binders
herbelin
2003-09-12
Mise en place affichage spécifique pour le scope des types
herbelin
2003-08-11
Nouvelle mouture du traducteur v7->v8
herbelin
2003-06-10
Ajout notation c.(f) en v8 pour les projections de Record; raffinement divers
herbelin
2003-04-29
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-07
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-03-21
*** empty log message ***
barras
2003-03-12
*** empty log message ***
barras
2003-02-05
Ajout du traducteur
desmettr