index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
Bug Double Inversion
herbelin
2003-10-27
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec alpha-c...
herbelin
2003-10-21
*
Correction bug FreshId
herbelin
2003-10-21
*
Globalisation des hints autorewrite
herbelin
2003-10-20
*
Extension de l'utilisation de contradiction
herbelin
2003-10-19
*
Extension de Contradiction au cas d'hypotheses ~A et A dans le contexte
herbelin
2003-10-18
*
subst marche dans les deux sens
filliatr
2003-10-17
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
Un Try supplementaire utile pour la compatibilite, car bring_hyps dans genera...
herbelin
2003-10-13
*
Deplacement next_global_ident_away dans Termops
herbelin
2003-10-13
*
Uniformisation comportement decompEq pour corriger un bug introduit dans le I...
herbelin
2003-10-11
*
Bug calcul du nom de la premiere equation
herbelin
2003-10-11
*
Death of 'a somewhat cryptic module'
herbelin
2003-10-11
*
Death of 'a somewhat cryptic module'
herbelin
2003-10-11
*
Typo
herbelin
2003-10-10
*
Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'
herbelin
2003-10-10
*
Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'
herbelin
2003-10-10
*
Dead of 'a somewhat cryptic module'
herbelin
2003-10-10
*
Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; p...
herbelin
2003-10-10
*
Unification lemInv et lemInv_in
herbelin
2003-10-10
*
Cablage en dur de inversion
herbelin
2003-10-10
*
Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'
herbelin
2003-10-10
*
Affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_repl...
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Bug utilisation nametab pour ltac
herbelin
2003-10-08
*
Des abbreviations pour constrintern.ml; generic argument IdentArg
herbelin
2003-10-08
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Correction bug NewInduction pour les inductifs de type 'ordinaux'
herbelin
2003-09-23
*
Bug internalisation des Extern: la globalisation doit etre stricte
herbelin
2003-09-23
*
Passage à la V8 par défaut
herbelin
2003-09-22
*
Interface Eauto
herbelin
2003-09-18
*
Indépendance vis à vis de Declare
herbelin
2003-09-12
*
Nettoyage
herbelin
2003-09-11
*
Protection traducteur contre meta de Grammar tactic
herbelin
2003-09-09
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
switching back to old tauto
corbinea
2003-07-03
*
added hints into Ground
corbinea
2003-07-02
*
suppression de newtauto
corbinea
2003-07-02
*
*** empty log message ***
courant
2003-06-27
*
Une completion de l'interpretation des TacAlias pour la partie interpretable
herbelin
2003-06-25
*
Ground Update.
corbinea
2003-06-20
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Ajout option Local à Hint, Hints et HintDestruct
herbelin
2003-06-14
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Ajout option translate_syntax pour caractériser l'interprétation du traduct...
herbelin
2003-06-12
*
Traducteur + passage des noms de tactiques à kernel_name pour compatibilité...
herbelin
2003-06-10
*
Ground and CCsolve updates
corbinea
2003-05-25
*
Amélioration affichage locations; prise en compte variables dans lettac; ajo...
herbelin
2003-05-24
*
Réparation d'un bug de backtracking qui lui-même succédait à une ineffica...
herbelin
2003-05-22
[next]