index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
pptactic.ml
Commit message (
Expand
)
Author
Age
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-29
*
Localisation erreurs TacAlias; Globalisation moins tolérante dans les
herbelin
2003-04-28
*
Reparation affichage LetTac
herbelin
2003-04-27
*
Localisation des appels de tactiques définies sans arguments
herbelin
2003-04-14
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
espace manquant
herbelin
2003-04-02
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
*** empty log message ***
barras
2003-03-12
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Ajout d'un suffixe "as [ names ]" pour nommer manuellement les
herbelin
2002-10-21
*
NewDestruct/NewInduction acceptent l'option "using"
herbelin
2002-10-21
*
L'application de ltac attend une référence; meilleure protection contre
herbelin
2002-10-14
*
Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage
herbelin
2002-10-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour
herbelin
2002-07-11
*
Petits beug d'affichages.
gregoire
2002-06-13
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29