index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
translate
/
pptacticnew.ml
Commit message (
Expand
)
Author
Age
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
petits changements de syntaxe
barras
2003-11-12
*
Traduction semantique des InHyp de clause en InHypValue si local def
herbelin
2003-11-09
*
'as' avant 'using' dans 'destruct'
herbelin
2003-11-09
*
Added Instantiate ... in
corbinea
2003-11-06
*
Divers bugs d'affichage
herbelin
2003-10-17
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
lettac -> set
barras
2003-10-16
*
pr_tactic sans traduction; affichage Inversion
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Ajout now_show
herbelin
2003-09-26
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
*
Système de renommage des noms de tactiques Ltac
herbelin
2003-09-22
*
Traduction de Instantiate
herbelin
2003-09-18
*
Passage de lconstr à constr pour les arguments immédiat de commandes
herbelin
2003-09-06
*
Bug et améliorations divers
herbelin
2003-08-31
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Formattage Apply with
herbelin
2003-06-23
*
Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'
herbelin
2003-06-19
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Raffinement divers
herbelin
2003-06-10
*
Ajout FreshId
herbelin
2003-05-24
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
coqide: toolbar/autosave
monate
2003-05-07
*
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
*
Aérer les := et : de "assert"
herbelin
2003-04-07
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
*** empty log message ***
barras
2003-03-12
*
Ajout du traducteur
desmettr
2003-02-05