diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 1c7a1932f..33fe8f1d1 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -177,3 +177,11 @@ module Vernac_ : end val reset_all_grammars : unit -> unit + +(* Registering/resetting the level of an entry *) + +val find_position : + bool -> Gramext.g_assoc option -> int option -> + Gramext.position option * Gramext.g_assoc option * string option + +val remove_levels : int -> unit |