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
*
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
*
Export de simplest_eapply, utilisé dans la contrib interface
notin
2007-04-16
*
fix bug with dependent inductive families
corbinea
2007-04-16
*
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
*
Proposition de correction pour le bug #1173 (ou du moins pour un
herbelin
2007-04-13
*
Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant
herbelin
2007-04-13
*
Extension to the general sequence operator (tactical). Now in addition to ...
emakarov
2007-04-02
*
Changement mineur du comportement de 'rewrite .. in * |-': si le
notin
2007-03-30
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
Suppression argument pattern_source du case_info (code jamais utilisé)
herbelin
2007-03-15
*
Correction bug #1439 (comportement de replace by)
notin
2007-03-13
*
Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...
herbelin
2007-02-24
*
Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme
herbelin
2007-02-22
*
Correction typo liée au commit 8779 (levait une anomalie)
herbelin
2007-02-21
*
Réparation absence d'interprétation des liaisons vers listes
herbelin
2007-02-15
*
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
herbelin
2007-02-13
*
bugfix suffices
corbinea
2007-02-09
*
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
*
Suppression de code mort
notin
2007-02-01
*
redirection of errors in coqide + dynamic warning printer (needed for tm_egg)
corbinea
2007-01-31
*
bugfix for suffices (support for open head)
corbinea
2007-01-29
*
finalized suffices
corbinea
2007-01-29
*
"suffices" implemented + syntax cleanup
corbinea
2007-01-28
*
decl mode: anonymous facts
corbinea
2007-01-25
*
Correction du bug #1315:
notin
2007-01-22
*
changes in declarative language : by term using tactic
corbinea
2007-01-22
*
Report correction bug #1289 dans trunk (r9435 pour branche v8.1)
herbelin
2006-12-26
*
remplacement d'un test d'egalite par un test de convertibilite dans injection...
jforest
2006-12-22
*
Dépliage du terme d'induction avant suppression quand celui-ci est un
herbelin
2006-12-13
*
Correction bug #1041 (double cause : non évitement des noms existants en
herbelin
2006-12-12
*
Changement dans le kernel :
bgregoir
2006-12-11
*
Raffinement de l'unification de "apply": mémorisation de certains
herbelin
2006-11-19
*
Ajout de dépliage de l'énoncé, si besoin est, dans apply in
herbelin
2006-11-10
*
Correction d'un bug refine
herbelin
2006-11-10
*
Quick hack to solve to complexity issue in function mark_occur
herbelin
2006-11-01
*
Retour sur la modification apportée en r9289, et nouvelle correction du bug ...
notin
2006-10-31
*
simplif de la partie ML de ring/field
barras
2006-10-27
*
Affichage d'un message d'erreur losque qu'une relation n'a pas été déclarÃ...
notin
2006-10-26
*
Petit bug apply in
herbelin
2006-10-26
*
Correction d'une tentative incorrecte (révision 9266) de clarification
herbelin
2006-10-25
*
Insère une coercion vers Sortclass dans 'contradiction' si nécessaire
herbelin
2006-10-24
*
Extension de la primitive ltac fresh pour qu'elle accepte une liste de
herbelin
2006-10-24
[next]