index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tactics.ml
Commit message (
Expand
)
Author
Age
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Bugfix in abstract_generalize
msozeau
2007-10-24
*
Uniformisation du comportement de rewrite et rewrite in : quand le
herbelin
2007-10-12
*
Ajout de eelim, ecase, edestruct et einduction (expérimental).
herbelin
2007-10-03
*
Add a new tactic to generalize an instantiated inductive predicate adding equ...
msozeau
2007-08-07
*
New intro pattern "@A", which generates a fresh name based on A.
glondu
2007-07-06
*
Retour à un message d'erreur d'apply qui montre un échec sans sans réduction
herbelin
2007-05-28
*
A fix for bug #1397:
letouzey
2007-05-23
*
Nouvelle stratégie d'unification des types des with-bindings dans
herbelin
2007-05-22
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
New keyword "Inline" for Parameters and Axioms for automatic
soubiran
2007-04-25
*
Suite unification apply et eapply (l'un et l'autre profite maintenant
herbelin
2007-04-16
*
Essai de partage de code entre apply et eapply
herbelin
2007-04-15
*
Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant
herbelin
2007-04-13
*
Report de la révision r9605 de la branche v8.1 vers le trunk (abstract récu...
notin
2007-02-09
*
Report de la révision 9599 de la v8.1 dans le trunk
notin
2007-02-06
*
Report correction bug #1289 dans trunk (r9435 pour branche v8.1)
herbelin
2006-12-26
*
Dépliage du terme d'induction avant suppression quand celui-ci est un
herbelin
2006-12-13
*
Changement dans le kernel :
bgregoir
2006-12-11
*
Ajout de dépliage de l'énoncé, si besoin est, dans apply in
herbelin
2006-11-10
*
Petit bug apply in
herbelin
2006-10-26
*
Correction d'une tentative incorrecte (révision 9266) de clarification
herbelin
2006-10-25
*
Ajout de la tactique "apply in".
herbelin
2006-10-24
*
Fixed "Show intros" which did not look at hypothesis.
courtieu
2006-10-23
*
Changement de comportement du [rewrite ... in H]: Coq échoue si H
notin
2006-10-03
*
Correction bug d'ordonnancement des hyps d'induction dans induction/destruct
herbelin
2006-09-01
*
Reparation bug Show intros: les hypothèses introduites précédemment
courtieu
2006-07-28
*
Correction du bug #1116
jforest
2006-07-20
*
amelioration du comportement de induction (retour a la version V8.0)
jforest
2006-07-18
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Correction bug du correctif bug assert as
herbelin
2006-05-02
*
Bug assert as
herbelin
2006-05-02
*
induction on multiple arguments made better:
courtieu
2006-04-12
*
adding a new tactic [intro_avoiding idl] which acts as intro but prevents the
jforest
2006-04-11
*
Enlevement de message d'erreur garbage.
courtieu
2006-04-06
*
ajout d'un rattrapage d'erreur pour "induction using".
courtieu
2006-04-05
*
+ destruct now works as induction on multiple arguments :
jforest
2006-03-21
*
-Debugging multiple induction, a bug appeared when having function
courtieu
2006-03-12
*
trying to fix a bug in pazrameter order in the multiple induction
coq
2006-02-23
*
cleaning
coq
2006-02-17
*
bug correction in the decomposition of an induction scheme.
coq
2006-02-17
*
changed the decomposition of an induction scheme
coq
2006-02-17
*
added isProd to term.mli.
coq
2006-02-16
*
continuing the generalization of "induction". Now induction schemes
coq
2006-02-15
*
induction now admits multiple induction arguments. The principle must
coq
2006-02-10
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
Backtrack commit précédent (incompatible avec le choix de prendre Idtac com...
herbelin
2006-01-21
[next]