Tactics Index

• ; 104
• ;[... |... |...] 105
• Abstract 108
• Absurd 14
• Apply 7
• Apply ...with 8
• Assumption 2
• Auto 80
• Binding list 13
• Case 39
• Case ...with 40
• Cbv 18
• Change 17
• Clear 3
• Compare 59
• Compute 20
• Constructor 28
• Constructor ...with 29
• Contradiction 15
• Conversion tactics 16
• Cut 11
• CutRewrite 53
• Decide Equality 58
• Decompose 44
• Decompose Record 46
• Decompose Sum 45
• Dependent Inversion 72
• Dependent Inversion ...with 74
• Dependent Inversion_clear 73
• Dependent Inversion_clear ...with 75
• Dependent Rewrite -> 66
• Dependent Rewrite <- 67
• Derive Inversion 79
• Destruct 41
• Discriminate 60 61
• Do 101
• Double Induction 43
• EApply 9 111
• EAuto 82
• ETrivial 83
• Elim 34
• Elim ...using 36
• Elim ...with 35
• ElimType 37
• Exact 0
• Exists 31
• Fail 100
• Fold 26
• Generalize 12
• Hints
  • Hint Unfold ident 96
  • Hint term 94
  • Immediate term 95
  • Print Hint 97
• Hnf 22
• Idtac 99
• Induction 38
• Info 107
• Injection 63 64
• Intro 4
• Intros 5 42
• Intros until 6
• Intuition 86
• Inversion 68 112
• Inversion ...in 70
• Inversion ...using 76
• Inversion ...using ...in 77
• Inversion_clear 69
• Inversion_clear ...in 71
• LApply 10
• Lazy 19
• Left 32
• Linear 87
• Linear with 88
• Omega 89 113
• Orelse 102
• Pattern 27
• Program 92 115
• Program_Expand 117
• Program_all 93 116
• Prolog 84
• Realizer 91 114
• Red 21
• Refine 1 110
• Reflexivity 55
• Repeat 103
• Replace ...with 54
• Rewrite 47
• Rewrite -> 48
• Rewrite -> ...in 51
• Rewrite <- 49
• Rewrite <- ...in 52
• Rewrite ...in 50
• Right 33
• Ring 90 118 119
• Simpl 23
• Simple Discriminate 62
• Simple Inversion 78
• Simplify_eq 65
• Split 30
• Symmetry 56
• Tacticals 98
• Tauto 85
• Transitivity 57
• Trivial 81
• Try 106
• Unfold 24
• Unfold ...in 25
• tactic macros 109