type hint =
(* tactics usage related hints *)
- | Use_ring_Luke
- | Use_fourier_Luke
- | Use_reflexivity_Luke
- | Use_symmetry_Luke
- | Use_assumption_Luke
- | Use_contradiction_Luke
- | Use_exists_Luke
- | Use_split_Luke
- | Use_left_Luke
- | Use_right_Luke
- | Use_apply_Luke of string (* use apply tactic on embedded term *)
+ | Use_ring
+ | Use_fourier
+ | Use_reflexivity
+ | Use_symmetry
+ | Use_assumption
+ | Use_contradiction
+ | Use_exists
+ | Use_split
+ | Use_left
+ | Use_right
+ | Use_apply of string (* use apply tactic on embedded term *)
(* hints list *)
| Hints of hint list