diff options
| author | Pierre-Marie Pédrot | 2016-03-17 14:01:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-17 14:38:45 +0100 |
| commit | 92a6a72ec4680d0f241e8b1ddd7b87f7ad11f65e (patch) | |
| tree | 808ea8702b5ddde7d6f84a366fc96d54cb985782 /parsing | |
| parent | 22c1e7c3f1d86902b1abf2d887e0e9bf93ddb60d (diff) | |
Relying on parsing rules rather than genarg to check if an argument is empty.
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 : |