diff options
| -rw-r--r-- | parsing/pcoq.ml4 | 6 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 3 |
2 files changed, 9 insertions, 0 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 473e095dc9..a6feeb473c 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -828,3 +828,9 @@ let rec interp_entry_name static up_level s sep = | Some t -> t | None -> ExtraArgType s in t, se + +let list_entry_names () = + let add_entry key (entry, _) accu = (key, entry) :: accu in + let ans = Hashtbl.fold add_entry (snd uprim) [] in + let ans = Hashtbl.fold add_entry (snd uconstr) ans in + Hashtbl.fold add_entry (snd utactic) ans diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index cf98e5a542..810a652dc0 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -282,6 +282,9 @@ val symbol_of_prod_entry_key : val interp_entry_name : bool (** true to fail on unknown entry *) -> int option -> string -> string -> entry_type * prod_entry_key +(** Recover the list of all known tactic notation entries. *) +val list_entry_names : unit -> (string * entry_type) list + (** Registering/resetting the level of a constr entry *) val find_position : |