aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Tactics.v
Commit message (Expand)AuthorAge
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* - Extracted from the tactic "now" an experimental tactic "easy" for smallGravatar herbelin2008-12-26
* Correction de bugs:Gravatar herbelin2008-08-05
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
* contradict can now handle False hypothesis in the spirit of contradictionGravatar letouzey2008-04-09
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* TypoGravatar notin2008-01-23
* Quelques arguments en plus...Gravatar glondu2007-12-17
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...Gravatar letouzey2007-11-06
* A way to specialize universally quantified hypothesis: if H is Gravatar letouzey2007-11-01
* Removed an extra \tacindex occurrence for the tactic discriminate.Gravatar emakarov2007-06-08
* Added back the tactics [apply -> ident], etc. to Tactics.v afterGravatar emakarov2007-04-02
* Removed the definition of extensions of apply to equivalencesGravatar emakarov2007-04-01
* Added new tactics for applying equivalences (iff) to Tactics.v:Gravatar emakarov2007-03-30
* stupid me: ?f two times in a patternGravatar letouzey2007-03-26
* Add f_equal case for 6 arguments.Gravatar msozeau2007-01-02
* Ajout de la tactique 'remember'Gravatar herbelin2006-10-24
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
* Ajout d'une valeur VList dans tacinterp pour permettre de cabler desGravatar herbelin2006-09-22
* incomplete and temporary fix for PR#1222: revert accepts up to 10 argsGravatar letouzey2006-09-21
* quelques raccourcis commodes + un f_equal plus efficaceGravatar letouzey2006-02-27
* *** empty log message ***Gravatar letouzey2005-08-26
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* quelques tactics ltacGravatar letouzey2005-02-23
* Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursGravatar herbelin2005-02-03