diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-10 19:46:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-10 23:13:45 +0200 |
| commit | f2983cec3544473b18ebc4d4e3a20b941decd196 (patch) | |
| tree | 0f0d76b21c427a0e77688e6eba01e7657991fed4 /parsing/pcoq.mli | |
| parent | bc3981687cd363820e35e5a2bd037d50e213f524 (diff) | |
Delimiting the use of unsafe code in Pcoq.
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 84f72ac55..72edab8f2 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -235,11 +235,6 @@ val set_command_entry : vernac_expr Gram.entry -> unit val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option -(** Binding general entry keys to symbols *) - -(** Recover the list of all known tactic notation entries. *) -val list_entry_names : unit -> (string * argument_type) list - (** Registering/resetting the level of a constr entry *) type gram_level = |