diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d320520015..8c3c299ade 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -288,3 +288,8 @@ val register_empty_levels : bool -> int list -> val remove_levels : int -> unit val level_of_snterml : Gram.symbol -> int + +(** TODO: remove me *) + +val of_coq_position : Extend.gram_position -> Compat.CompatGramext.position +val of_coq_assoc : Extend.gram_assoc -> Compat.CompatGramext.assoc |