index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
syntax
/
PPTactic.v
Commit message (
Expand
)
Author
Age
*
Affichage NewInduction/NewDesctruct
herbelin
2001-12-13
*
Affichage des '_' pour Intros
herbelin
2001-12-06
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...
herbelin
2001-10-05
*
Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction
herbelin
2001-08-05
*
Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...
herbelin
2001-06-25
*
Reorganisation pour Ltac
delahaye
2001-04-24
*
Ajout de syntaxe pour Ltac
delahaye
2001-04-23
*
Reparation de l'affichage des THEN's
delahaye
2001-04-13
*
Bug affichage LETPATTERN
herbelin
2001-04-10
*
Interprétation des qualidarg
herbelin
2001-03-27
*
Les règles d'affichage ajoutés dans le commit précédent avait le même no...
herbelin
2001-03-23
*
Règle de syntaxe pour CASTEDCOMMAND
herbelin
2001-03-22
*
entetes
filliatr
2001-03-15
*
Ajout du Match Context
delahaye
2001-02-07
*
Traitement du pretty-print des Redexp
delahaye
2000-11-21
*
Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...
herbelin
2000-10-18
*
Renommage tactique Let en LetTac
herbelin
2000-10-03
*
Renommage command en constr
herbelin
2000-01-07
*
MAJ
herbelin
1999-12-06
*
pretty-print
filliatr
1999-12-05