diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 14 |
2 files changed, 14 insertions, 1 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 19ae97da77..759e60fbca 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -439,7 +439,6 @@ module Module = let module_expr = Entry.create "module_expr" let module_type = Entry.create "module_type" end - let epsilon_value f e = let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in let ext = [None, None, [r]] in diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 352857d4cd..3203a25b46 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -41,6 +41,16 @@ end - static rules explicitly defined in files g_*.ml4 - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and VERNAC EXTEND (see e.g. file extratactics.ml4) + + Note that parsing a Coq document is in essence stateful: the parser + needs to recognize commands that start proofs and use a different + parsing entry point for them. + + We thus provide two different interfaces: the "raw" parsing + interface, in the style of camlp5, which provides more flexibility, + and a more specialize "parse_vernac" one, which will indeed adjust + the state as needed. + *) (** Dynamic extension of rules @@ -269,3 +279,7 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry val register_grammars_by_name : string -> any_entry list -> unit val find_grammars_by_name : string -> any_entry list + +(** Parsing state handling *) +val freeze : marshallable:bool -> frozen_t +val unfreeze : frozen_t -> unit |