From 1cfec06ce06ae6c783b840a8d59bb89ee34a87ee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 17 May 2014 18:51:11 +0200
Subject: Adding way to get the list of the accepted tactic notation arguments.

---
 parsing/pcoq.ml4 | 6 ++++++
 parsing/pcoq.mli | 3 +++
 2 files changed, 9 insertions(+)

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 :
-- 
cgit v1.2.3