index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
pptactic.mli
Commit message (
Expand
)
Author
Age
*
Correction printer des Tactic Notation
herbelin
2005-12-23
*
Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...
herbelin
2005-12-21
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Nouvelle en-tête
herbelin
2004-07-16
*
Simplification afficheur de tactiques non primitive
herbelin
2003-09-18
*
Traduction des réferences arguments de commandes non primitives
herbelin
2003-09-09
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
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-12
*
Debugger plus informatif
delahaye
2003-02-13
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29