diff options
| author | Pierre-Marie Pédrot | 2014-05-17 18:51:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-17 20:04:10 +0200 |
| commit | 1cfec06ce06ae6c783b840a8d59bb89ee34a87ee (patch) | |
| tree | f2c9c6a5edb03dae260f1a64dd07d67ea49b753e | |
| parent | ea3537acee72a521c8e7537da42445d603889809 (diff) | |
Adding way to get the list of the accepted tactic notation arguments.
| -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 : |