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
*
moved instantiate binding to extratactics
corbinea
2004-06-29
*
more evar stuff
corbinea
2004-06-28
*
Bug affichage ClearBody
herbelin
2004-05-27
*
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...
herbelin
2004-03-17
*
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...
herbelin
2004-03-17
*
Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...
herbelin
2004-03-02
*
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...
herbelin
2004-03-02
*
Généralisation du type ltac Identifier en IntroPattern; prise en compte des...
herbelin
2004-03-01
*
bugs avec Pose et Assert
barras
2004-01-09
*
Bug affichage Decompose
herbelin
2003-12-24
*
ajout test de non-regression Clear d'une def locale
barras
2003-12-17
*
Nouvelle tactique EExists
clrenard
2003-12-01
*
Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...
herbelin
2003-11-25
*
New tactics : econstructor, eleft, eright, esplit
clrenard
2003-11-17
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Mise en place systeme de renommage des noms de variables liees dans la biblio...
herbelin
2003-11-12
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
Traduction semantique des InHyp de clause en InHypValue si local def
herbelin
2003-11-09
*
Added Instantiate ... in
corbinea
2003-11-06
*
Le printeur de Show Script n'etait pas le bon en v7
herbelin
2003-11-02
*
Traduction des noms pour les refs de pr_glob_generic (via pr_global)
herbelin
2003-11-01
*
Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par...
herbelin
2003-10-21
*
Traduction des idents aussi dans le printer generique des tactiques
herbelin
2003-10-17
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
Cablage en dur de inversion
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Simplification afficheur de tactiques non primitive
herbelin
2003-09-18
*
En attendant l'afficheur...
herbelin
2003-09-16
*
Traduction des réferences arguments de commandes non primitives
herbelin
2003-09-09
*
Bug affichage tactiques supplementaires en v8 (suite)
herbelin
2003-09-06
*
Bug affichage tactiques supplementaires en v8
herbelin
2003-09-05
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
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
*
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
[next]