- | "alias" -> mode := `Alias
- | "term" -> mode := `Term
- | "tactic" -> mode := `Tactic
- | "tactical" -> mode := `Tactical
+ | "alias" -> prerr_endline "Alias"; `Alias
+ | "term" -> prerr_endline "Term"; `Term
+ | "tactic" -> prerr_endline "Tactic"; `Tactic
+ | "tactical" -> prerr_endline "Tactical"; `Tactical