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 (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...
herbelin
2004-01-27
*
Bug induction lors de types inductives avec parametres
herbelin
2004-01-23
*
bugs avec Pose et Assert
barras
2004-01-09
*
Reparation incompatibilites v7/v8 dans destruct; utilisation de noms t2_3 dan...
herbelin
2003-12-23
*
*** empty log message ***
barras
2003-12-23
*
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-12-15
*
Correction bug soumis par Yves
herbelin
2003-12-13
*
Nouvelle tactique EExists
clrenard
2003-12-01
*
Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...
herbelin
2003-11-25
*
Prise en compte des defs syntaxiques dans is_global et global_reference qui p...
herbelin
2003-11-24
*
Bug introduit avec le 'Simpl f'
herbelin
2003-11-22
*
Blindage vis a vis des constructeurs partiellement appliques
herbelin
2003-11-18
*
New tactics : econstructor, eleft, eright, esplit
clrenard
2003-11-17
*
Bug nommage destruct
herbelin
2003-11-15
*
Move des hyps de NewInduction: retour a situation V7.4 a defaut d'etre robuste
herbelin
2003-11-14
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Prise en compte des alias syntaxiques vers des references dans divers lieux d...
herbelin
2003-11-12
*
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
[next]