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
*
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
*
Traduction semantique des InHyp de clause en InHypValue si local def; simplif...
herbelin
2003-11-09
*
'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ...
herbelin
2003-11-09
*
Code obsolete
herbelin
2003-11-08
*
Nettoyage
herbelin
2003-11-08
*
Added Instantiate ... in
corbinea
2003-11-06
*
Amelioration message d'erreur avec pretyping; prise en compte syntactic def d...
herbelin
2003-11-04
*
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
[next]