diff options
| author | Pierre-Marie Pédrot | 2019-03-31 23:08:57 +0200 |
|---|---|---|
| committer | GitHub | 2019-03-31 23:08:57 +0200 |
| commit | 5a2b4b1f084bb749c7f43b4f592ea161d7ca968b (patch) | |
| tree | f5ec1a5aa1e9d80cb5aa6844588dd646526f9a40 | |
| parent | 66c0cf22a9f67b70046674fb066942a5556c1558 (diff) | |
| parent | 93524ed2dfb3bbcc2006286954001039c95732cd (diff) | |
Merge pull request coq/ltac2#112 from gares/quotations
overlay for PR 9733
| -rw-r--r-- | src/g_ltac2.mlg | 8 | ||||
| -rw-r--r-- | src/tac2core.ml | 2 | ||||
| -rw-r--r-- | src/tac2entries.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg index a404227d3d..2483ef459a 100644 --- a/src/g_ltac2.mlg +++ b/src/g_ltac2.mlg @@ -831,7 +831,7 @@ let open Tok in let (++) r s = Next (r, s) in let rules = [ Rule ( - Stop ++ Aentry test_dollar_ident ++ Atoken (KEYWORD "$") ++ Aentry Prim.ident, + Stop ++ Aentry test_dollar_ident ++ Atoken (pattern_for_KEYWORD "$") ++ Aentry Prim.ident, begin fun id _ _ loc -> let id = Loc.tag ~loc id in let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in @@ -840,7 +840,7 @@ let rules = [ ); Rule ( - Stop ++ Aentry test_ampersand_ident ++ Atoken (KEYWORD "&") ++ Aentry Prim.ident, + Stop ++ Aentry test_ampersand_ident ++ Atoken (pattern_for_KEYWORD "&") ++ Aentry Prim.ident, begin fun id _ _ loc -> let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in @@ -849,8 +849,8 @@ let rules = [ ); Rule ( - Stop ++ Atoken (IDENT "ltac2") ++ Atoken (KEYWORD ":") ++ - Atoken (KEYWORD "(") ++ Aentry tac2expr ++ Atoken (KEYWORD ")"), + Stop ++ Atoken (pattern_for_IDENT "ltac2") ++ Atoken (pattern_for_KEYWORD ":") ++ + Atoken (pattern_for_KEYWORD "(") ++ Aentry tac2expr ++ Atoken (pattern_for_KEYWORD ")"), begin fun _ tac _ _ _ loc -> let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) diff --git a/src/tac2core.ml b/src/tac2core.ml index 30beee58de..0f85f56c22 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -1251,7 +1251,7 @@ open CAst let () = add_scope "keyword" begin function | [SexprStr {loc;v=s}] -> - let scope = Extend.Atoken (Tok.KEYWORD s) in + let scope = Extend.Atoken (Tok.pattern_for_KEYWORD s) in Tac2entries.ScopeRule (scope, (fun _ -> q_unit)) | arg -> scope_fail "keyword" arg end diff --git a/src/tac2entries.ml b/src/tac2entries.ml index 3073aad84f..bce58653e6 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -539,7 +539,7 @@ let parse_scope = function CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id) | SexprStr {v=str} -> let v_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) in - ScopeRule (Extend.Atoken (Tok.IDENT str), (fun _ -> v_unit)) + ScopeRule (Extend.Atoken (Tok.pattern_for_IDENT str), (fun _ -> v_unit)) | tok -> let loc = loc_of_token tok in CErrors.user_err ?loc (str "Invalid parsing token") |