diff options
| author | Pierre-Marie Pédrot | 2017-08-29 01:16:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-29 01:23:32 +0200 |
| commit | db03c10aaafd3c0128a5b7504f14d4b7aaca842e (patch) | |
| tree | 47ee736fc51f6e309cad5aa26158eafcf83f06e0 /src | |
| parent | ece1cc059c26351d05a0ef41131c663c37cb7761 (diff) | |
Implementing Ltac2 antiquotations in constr syntax.
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 14 | ||||
| -rw-r--r-- | src/tac2quote.ml | 5 | ||||
| -rw-r--r-- | src/tac2quote.mli | 3 |
3 files changed, 22 insertions, 0 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index ae7e255896..672db12f1d 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -64,6 +64,16 @@ let test_ampersand_ident = | _ -> err ()) | _ -> err ()) +let test_dollar_ident = + Gram.Entry.of_parser "test_dollar_ident" + (fun strm -> + match stream_nth 0 strm with + | IDENT "$" | 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" @@ -649,6 +659,10 @@ GEXTEND Gram 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)) + | test_dollar_ident; "$"; id = Prim.ident -> + let tac = Tac2quote.of_exact_var ~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)) ] ] ; END diff --git a/src/tac2quote.ml b/src/tac2quote.ml index dbd2fd0529..f87e370032 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -233,6 +233,11 @@ let of_exact_hyp ?loc id = let refine = CTacRef (AbsKn (TacConstant (control_core "refine"))) in CTacApp (loc, refine, [thunk (of_hyp ~loc id)]) +let of_exact_var ?loc id = + let loc = Option.default dummy_loc loc in + let refine = CTacRef (AbsKn (TacConstant (control_core "refine"))) in + CTacApp (loc, refine, [thunk (of_variable id)]) + let of_dispatch tacs = let loc = Option.default dummy_loc (fst tacs) in let default = function diff --git a/src/tac2quote.mli b/src/tac2quote.mli index 7f3d9dce6e..b2687f01a3 100644 --- a/src/tac2quote.mli +++ b/src/tac2quote.mli @@ -58,6 +58,9 @@ val of_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr val of_exact_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr (** id ↦ 'Control.refine (fun () => Control.hyp @id') *) +val of_exact_var : ?loc:Loc.t -> Id.t located -> raw_tacexpr +(** id ↦ 'Control.refine (fun () => Control.hyp @id') *) + val of_dispatch : dispatch -> raw_tacexpr val of_strategy_flag : strategy_flag -> raw_tacexpr |