diff options
| -rw-r--r-- | parsing/egramcoq.ml | 27 | ||||
| -rw-r--r-- | parsing/egramcoq.mli | 8 |
2 files changed, 35 insertions, 0 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 9905a5ad4..2e83c2b6b 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -343,3 +343,30 @@ let with_grammar_rule_protection f x = let reraise = Errors.push reraise in let () = unfreeze fs in raise reraise + +(**********************************************************************) +(** Ltac quotations *) + +let ltac_quotations = ref String.Set.empty + +let create_ltac_quotation name cast wit e = + let () = + if String.Set.mem name !ltac_quotations then + failwith ("Ltac quotation " ^ name ^ " already registered") + in + let () = ltac_quotations := String.Set.add name !ltac_quotations in +(* let level = Some "1" in *) + let level = None in + let assoc = Some (of_coq_assoc Extend.RightA) in + let rule = [ + gram_token_of_string name; + gram_token_of_string ":"; + symbol_of_prod_entry_key (Agram (Gram.Entry.obj e)); + ] in + let action v _ _ loc = + let loc = !@loc in + let arg = TacGeneric (Genarg.in_gen (Genarg.rawwit wit) (cast (loc, v))) in + TacArg (loc, arg) + in + let gram = (level, assoc, [rule, Gram.action action]) in + maybe_uncurry (Gram.extend Tactic.tactic_expr) (None, [gram]) diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 91a636306..7cf3bab69 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -66,3 +66,11 @@ val recover_notation_grammar : notation_var_internalization_type list * notation_grammar val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b + +(** Adding tactic quotations *) + +val create_ltac_quotation : string -> ('grm Loc.located -> 'raw) -> + ('raw, 'glb, 'top) genarg_type -> 'grm Gram.entry -> unit +(** [create_ltac_quotation name f wit e] adds a quotation rule to Ltac, that is, + Ltac grammar now accepts arguments of the form ["name" ":" <e>], and + generates a generic argument using [f] on the entry parsed by [e]. *) |