diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 69ba57d516..352857d4cd 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -13,7 +13,6 @@ open Extend open Genarg open Constrexpr open Libnames -open Gramlib (** The parser of Coq *) @@ -261,11 +260,6 @@ val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b -(** Location Utils *) -val of_coqloc : Loc.t -> Ploc.t -val to_coqloc : Ploc.t -> Loc.t -val (!@) : Ploc.t -> Loc.t - type frozen_t val parser_summary_tag : frozen_t Summary.Dyn.tag |