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