- | Use_ring_Luke -> Tactics.ring ()
- | Use_fourier_Luke -> Tactics.fourier ()
- | Use_reflexivity_Luke -> Tactics.reflexivity ()
- | Use_symmetry_Luke -> Tactics.symmetry ()
- | Use_assumption_Luke -> Tactics.assumption ()
- | Use_contradiction_Luke -> Tactics.contradiction ()
- | Use_exists_Luke -> Tactics.exists ()
- | Use_split_Luke -> Tactics.split ()
- | Use_left_Luke -> Tactics.left ()
- | Use_right_Luke -> Tactics.right ()
- | Use_apply_Luke term ->
+ | Use_ring -> Tactics.ring ()
+ | Use_fourier -> Tactics.fourier ()
+ | Use_reflexivity -> Tactics.reflexivity ()
+ | Use_symmetry -> Tactics.symmetry ()
+ | Use_assumption -> Tactics.assumption ()
+ | Use_contradiction -> Tactics.contradiction ()
+ | Use_exists -> Tactics.exists ()
+ | Use_split -> Tactics.split ()
+ | Use_left -> Tactics.left ()
+ | Use_right -> Tactics.right ()
+ | Use_apply term ->