SEP SYMBOL ";";
goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
let goal_path =
- match goal_path with
- None -> Ast.UserInput
- | Some goal_path -> goal_path
+ match goal_path, hyp_paths with
+ None, [] -> Ast.UserInput
+ | None, _::_ -> Ast.Implicit
+ | Some goal_path, _ -> goal_path
in
hyp_paths,goal_path
]