diff options
| author | Pierre-Marie Pédrot | 2017-08-25 14:51:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-25 14:51:57 +0200 |
| commit | c3d83f8437022986593df45c3c3920c8356d9f84 (patch) | |
| tree | cef3d34fc904e8490c1e24b1a206156b4016ab5d /src | |
| parent | 72f47973b860c8074aa976759ee1adce993dac49 (diff) | |
Lookahead to cheat the constr parser in order to parse "& IDENT".
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 7406a45207..3d873c7369 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -54,6 +54,16 @@ let test_lpar_id_rpar = | _ -> err ()) | _ -> err ()) +let test_ampersand_ident = + Gram.Entry.of_parser "test_ampersand_ident" + (fun strm -> + match stream_nth 0 strm with + | KEYWORD "&" -> + (match stream_nth 1 strm with + | IDENT _ -> () + | _ -> err ()) + | _ -> err ()) + let tac2expr = Tac2entries.Pltac.tac2expr let tac2type = Gram.entry_create "tactic:tac2type" let tac2def_val = Gram.entry_create "tactic:tac2def_val" @@ -617,8 +627,8 @@ GEXTEND Gram [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg)) - | "&"; id = [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] -> - let tac = Tac2quote.of_exact_hyp ~loc:!@loc id in + | test_ampersand_ident; "&"; id = Prim.ident -> + let tac = Tac2quote.of_exact_hyp ~loc:!@loc (Loc.tag ~loc:!@loc id) in let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg)) ] ] |