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
*
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
*
Ajout de la tactique "apply in".
herbelin
2006-10-24
*
Interprétation du terme comme type dans 'change' si pas de 'with' (pour bén...
herbelin
2006-10-24
*
Fixed "Show intros" which did not look at hypothesis.
courtieu
2006-10-23
*
Correction du bug #1255 (réécriture setoid sous un produit)
notin
2006-10-20
*
affichage des ... dans les scripts
barras
2006-10-16
*
revision de la semantique de rewrite ... in <clause>. details dans la doc
letouzey
2006-10-05
*
Changement de comportement du [rewrite ... in H]: Coq échoue si H
notin
2006-10-03
*
Retour sur la suppression du pf_nf (trop d'exemples utilisent avec
herbelin
2006-10-03
*
Une passe sur l'injection et la discrimination...
herbelin
2006-10-01
*
Suppression de la comparaison (inutile) des paramètres globaux des
herbelin
2006-09-30
*
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
barras
2006-09-26
*
fixed error mesg in decl mode
corbinea
2006-09-26
*
Permet a un unfold de recevoir ses occurences a travers une variable Ltac.
letouzey
2006-09-25
*
Correction bug #1229 (toplevel "unresolved evar" fled through
herbelin
2006-09-23
*
Ajout d'une valeur VList dans tacinterp pour permettre de cabler des
herbelin
2006-09-22
*
Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter s...
herbelin
2006-09-21
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Indentation + svnprop
notin
2006-09-12
*
Correction bug d'ordonnancement des hyps d'induction dans induction/destruct
herbelin
2006-09-01
*
improve the amount of information given by the Ltac tactic debugger
bertot
2006-08-28
*
Bug in replace tactics introduced in r9073 (overlap between replace .. with a...
jforest
2006-08-23
*
Forgot a file in previous commit
jforest
2006-08-22
*
+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no
jforest
2006-08-22
*
corrects an error in the substitution of module paths inside tactics:
bertot
2006-08-17
*
Reparation bug Show intros: les hypothèses introduites précédemment
courtieu
2006-07-28
[next]