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
*
Prise en compte des notations "alias" dans la globalisation des coercions.
herbelin
2007-11-08
*
Réparation d'une inefficacité bêtement introduite dans la révision
herbelin
2007-10-27
*
Bugfix in abstract_generalize
msozeau
2007-10-24
*
- Préservation des appels récursifs de tête dans ltac (réponse au "wish"
herbelin
2007-10-12
*
Uniformisation du comportement de rewrite et rewrite in : quand le
herbelin
2007-10-12
*
Allowing setoid_reflexivity_in to work on quantified hypothesis (bug #1710)
letouzey
2007-10-10
*
Added the automatic generation of the boolean equality if possible and the
vsiles
2007-10-05
*
Ajout de eelim, ecase, edestruct et einduction (expérimental).
herbelin
2007-10-03
*
Correcting error message when adding Setoid, Relation or morphism (bug #1626)
jforest
2007-10-02
*
Suite de 10157
herbelin
2007-09-30
*
Ajout infos de débogage de "universe inconsistency" quand option Set
herbelin
2007-09-30
*
On empêche "fresh" d'engendrer un mot-clé.
herbelin
2007-09-28
*
Découpage de Setoid.v
notin
2007-09-27
*
- Fixing bug 1703 ("intros until n" falls back on the variable name when
herbelin
2007-09-21
*
Raffinement de l'algorithme d'inférence de type
herbelin
2007-09-17
*
Uniformisation politique de nommage evd/isevars (evd si evar_defs,
herbelin
2007-09-06
*
Correction du bug #1634 + ajout de bugs dans la test-suite
notin
2007-08-22
*
Correction du bug #1322
notin
2007-08-16
*
Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;
notin
2007-08-16
*
Add a new tactic to generalize an instantiated inductive predicate adding equ...
msozeau
2007-08-07
*
Declarative language: fixed the generation of fixpoints for induction proofs.
corbinea
2007-07-24
*
Raffinement de interp_ident pour que l'ident interprété soit au choix
herbelin
2007-07-18
*
Slight cleanup of refl_omega.ml : in particular it uses now list
letouzey
2007-07-11
*
Adding a syntax for "n-ary" rewrite:
letouzey
2007-07-06
*
extension of the rename tactic: the following is now allowed:
letouzey
2007-07-06
*
New intro pattern "@A", which generates a fresh name based on A.
glondu
2007-07-06
*
killing some more non-exhaustive patterns
letouzey
2007-06-26
*
ajout de head0 et tail0 en natif
bgregoir
2007-06-20
*
Correction d'un bug dans l'affichage du message d'erreur real_clean
herbelin
2007-05-29
*
Contrôle de la compatibilité de apply via une information dans les
herbelin
2007-05-28
*
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
*
Backtrack sur l'effacement dans le contexte de but des lieurs
herbelin
2007-05-19
*
Interprétation des listes de VarArgType dans les notations faisant
herbelin
2007-05-18
*
Wish #1582 (3eme)
herbelin
2007-05-18
*
Quelques essais autour du wish implicite au rapport de bug #1582 (2eme)
herbelin
2007-05-18
*
Quelques essais autour du wish implicite au rapport de bug #1582
herbelin
2007-05-18
*
correction de bug dans Function et augmentation de la classe des fonctions su...
jforest
2007-05-17
*
Correction des bugs #1537 (anomalie sur signature incomplète) et #1536
herbelin
2007-05-17
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Multiples changements autour des implicites :
herbelin
2007-04-29
*
Ajout de la possibilité de faire référence dans certains cas à un nom
herbelin
2007-04-28
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
fixed glitch in escape
corbinea
2007-04-27
*
fin des conclusions multiples
corbinea
2007-04-26
*
New keyword "Inline" for Parameters and Axioms for automatic
soubiran
2007-04-25
*
debug plus poussé induction dépendante
corbinea
2007-04-18
*
- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771
herbelin
2007-04-18
[next]