index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Init
/
Tactics.v
Commit message (
Expand
)
Author
Age
*
Updating headers.
herbelin
2012-08-08
*
induction/destruct : nicer syntax for generating equations (solves #2741)
letouzey
2012-07-09
*
Notation: a new annotation "compat 8.x" extending "only parsing"
letouzey
2012-07-05
*
Modularization of BinNat + fixes of stdlib
letouzey
2011-05-05
*
Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed
herbelin
2011-04-28
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Bool: shorter and more systematic proofs + an iff lemma about eqb
letouzey
2010-07-16
*
clear/revert dependent: restrict to hyp(h) instead of ident(h)
letouzey
2010-06-18
*
New tactic "clear dependent", for the moment in ltac in Init/Tactics
letouzey
2010-06-17
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'
letouzey
2009-10-08
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
New tactic to rewrite decidability lemmas when one knows which side
herbelin
2009-08-24
*
Miscellaneous practical commits:
herbelin
2009-06-29
*
- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",
herbelin
2009-01-02
*
- Another bug in get_sort_family_of (sort-polymorphism of constants and
herbelin
2008-12-28
*
- Extracted from the tactic "now" an experimental tactic "easy" for small
herbelin
2008-12-26
*
Correction de bugs:
herbelin
2008-08-05
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la
herbelin
2008-04-29
*
contradict can now handle False hypothesis in the spirit of contradiction
letouzey
2008-04-09
*
f_equal, revert, specialize in ML, contradict in better Ltac (+doc)
letouzey
2008-03-07
*
Typo
notin
2008-01-23
*
Quelques arguments en plus...
glondu
2007-12-17
*
small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is
letouzey
2007-11-06
*
Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...
letouzey
2007-11-06
*
A way to specialize universally quantified hypothesis: if H is
letouzey
2007-11-01
*
Removed an extra \tacindex occurrence for the tactic discriminate.
emakarov
2007-06-08
*
Added back the tactics [apply -> ident], etc. to Tactics.v after
emakarov
2007-04-02
*
Removed the definition of extensions of apply to equivalences
emakarov
2007-04-01
*
Added new tactics for applying equivalences (iff) to Tactics.v:
emakarov
2007-03-30
*
stupid me: ?f two times in a pattern
letouzey
2007-03-26
*
Add f_equal case for 6 arguments.
msozeau
2007-01-02
*
Ajout de la tactique 'remember'
herbelin
2006-10-24
*
revision de la semantique de rewrite ... in <clause>. details dans la doc
letouzey
2006-10-05
*
Ajout d'une valeur VList dans tacinterp pour permettre de cabler des
herbelin
2006-09-22
*
incomplete and temporary fix for PR#1222: revert accepts up to 10 args
letouzey
2006-09-21
*
quelques raccourcis commodes + un f_equal plus efficace
letouzey
2006-02-27
*
*** empty log message ***
letouzey
2005-08-26
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
quelques tactics ltac
letouzey
2005-02-23
*
Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs
herbelin
2005-02-03