diff options
| author | Hugo Herbelin | 2015-12-09 23:38:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 17:44:19 +0100 |
| commit | fb77937a6ba0fe45e978911db08de57f931683e1 (patch) | |
| tree | 7a82660e8a0686d4989a615bf5c839ec2e7d8c60 /parsing | |
| parent | 20e1829ad3de42dd322af972c6f9a585f40738ef (diff) | |
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Marking it as experimental.
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 |