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
*
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
*
Ajout de la contrainte de résoudre l'assertion dans 'assert by'
herbelin
2006-01-20
*
Conséquences supplémentaires de la fin du support v7
herbelin
2006-01-19
*
Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq
herbelin
2006-01-16
*
Code redondant
herbelin
2006-01-16
*
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
herbelin
2006-01-16
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Réparation bug #1000 (attendre fin de toutes les intros avant d'effacer les ...
herbelin
2005-09-08
*
Correction double bug #986: Fold ne préserve pas nécessairement le typage e...
herbelin
2005-07-13
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
Ajout de l'axiome du but prouve par la tactique simplifi
coq
2005-03-22
*
Le type d'un Let est considéré comme 'user-provided' par le noyau et doit d...
herbelin
2005-03-19
*
Report depuis la V8.0pl2 de la correction d'un bug du traducteur
herbelin
2005-03-19
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...
herbelin
2005-01-02
*
Bug 'set n in * |-'
herbelin
2004-12-04
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
Restructuration fonctions de réécriture depuis égalité dépendante; facto...
herbelin
2004-10-27
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
[next]