- just = OPT [ IDENT "by"; by =
- [ univ = tactic_term_list1 -> `Univ univ
- | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
- | SYMBOL "_" -> `Trace ] -> by ] -> just,params
+ just = OPT [ is_user_trace =
+ [ IDENT "by" -> true
+ | IDENT "trace" -> false ];
+ by =
+ [ univ = tactic_term_list1 -> `Univ univ
+ | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
+ | SYMBOL "_" -> `Trace ] -> is_user_trace,by ] -> just,params