- tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> tl,
- (* (match tl with Some l -> l | None -> []), *)
- params
- ]
-];
- nauto_params: [
- [ params =
- LIST0 [
- i = auto_fixed_param -> i,""
- | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
- string_of_int v | v = IDENT -> v ] -> i,v ] ->
- params
+ just = OPT [ IDENT "by"; by =
+ [ univ = tactic_term_list1 -> `Univ univ
+ | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
+ | SYMBOL "_" -> `Trace ] -> by ] -> just,params