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
*
encore un correctif sur le rewrite H in setoid:
letouzey
2006-05-05
*
Extension syntaxique de rewrite in: au lieu de pouvoir faire
letouzey
2006-05-02
*
Changement de comportement de rewrite: face a une egalité setoid, on
letouzey
2006-05-02
*
Correction bug du correctif bug assert as
herbelin
2006-05-02
*
Bug assert as
herbelin
2006-05-02
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...
notin
2006-04-28
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Diverses corrections de l'afficheur et du traducteur pour s'assurer de
herbelin
2006-04-26
*
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
*
resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses
letouzey
2006-04-05
*
ajout d'un rattrapage d'erreur pour "induction using".
courtieu
2006-04-05
*
Correction bug 1119 (inversion marche a moitie dans Type)
herbelin
2006-04-02
*
Made pretyping a functor over a coercion implementation. Pretyping.Default us...
msozeau
2006-03-22
*
- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de
herbelin
2006-03-22
*
+ 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
*
Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...
herbelin
2006-03-05
*
Correction bug #1097 (dû à une typo...)
herbelin
2006-03-02
*
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
*
Debugging en syntaxe v8
herbelin
2006-02-05
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
Ajout option 'using lemmas' à auto/trivial/eauto
herbelin
2006-01-28
*
Suppression code pour hints nommés à la V7 (voire à la V6...)
herbelin
2006-01-28
*
Suppression de la dépendance en Map.fold de ocaml dont la sémantique a
herbelin
2006-01-24
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...
herbelin
2006-01-21
*
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
*
Export eassumption
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
*
Standardisation du nom de subst_raw en subst_rawconstr
herbelin
2006-01-11
*
Standardisation du nom de subst_raw en subst_rawconstr
herbelin
2006-01-11
*
Résidus du traducteur v7 -> v8
herbelin
2006-01-11
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Ajout paramétricité du nom de la base de hint dans auto et trivial
herbelin
2006-01-11
*
Nettoyage coqlib
herbelin
2005-12-30
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Petite correction nom QuantHypArgType suite suppression traducteur
herbelin
2005-12-26
[next]