diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml | 7 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
2 files changed, 9 insertions, 0 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index cf65262c4a..52437e3867 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -853,3 +853,10 @@ let list_entry_names () = let ans = Hashtbl.fold add_entry (get_utable uprim) [] in let ans = Hashtbl.fold add_entry (get_utable uconstr) ans in Hashtbl.fold add_entry (get_utable utactic) ans + +let epsilon_value f e = + let r = Rule (Next (Stop, e), fun x _ -> f x) in + let ext = of_coq_extend_statement (None, [None, None, [r]]) in + let entry = G.entry_create "epsilon" in + let () = maybe_uncurry (Gram.extend entry) ext in + try Some (parse_string entry "") with _ -> None diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index b26c3044bd..7e0c89fd12 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -272,6 +272,8 @@ val symbol_of_constr_prod_entry_key : gram_assoc option -> val name_of_entry : 'a Gram.entry -> 'a Entry.t +val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option + (** Binding general entry keys to symbols *) type 's entry_name = EntryName : |