diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 4d42dfe85a..3d59b9b8db 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -311,7 +311,8 @@ GEXTEND Gram | "**" -> !@loc, IntroForthcoming false ]] ; simple_intropattern: - [ [ pat = simple_intropattern_closed; l = LIST0 ["/"; c = constr -> c] -> + [ [ pat = simple_intropattern_closed; + l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> let loc0,pat = pat in let f c pat = let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in |