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
*
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
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Prise en compte de l'information que certaines tactiques attendent un type (u...
herbelin
2005-12-21
*
Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...
herbelin
2005-12-21
*
Changement des named_context
gregoire
2005-12-02
*
A la demande de Julien Forest
letouzey
2005-11-17
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Confusion message erreur détectée par nouveau warning X de ocaml 3.09
herbelin
2005-11-04
[next]