diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index afe8889096..d320520015 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -268,10 +268,6 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** Binding general entry keys to symbols *) -type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry - -val get_entry : gram_universe -> string -> typed_entry - (** Recover the list of all known tactic notation entries. *) val list_entry_names : unit -> (string * argument_type) list |