diff options
| author | Pierre-Marie Pédrot | 2016-04-24 17:35:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-24 19:16:33 +0200 |
| commit | b1f95532137644d55b9018da80f9ffe63b289023 (patch) | |
| tree | cfb8531dbcd8a6abc0ad44ef975e8a79373aa766 /ltac | |
| parent | ea984528e269fa34afa3dd1757a00ff5a8405157 (diff) | |
Remove dead registering code in Pcoq.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacentries.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 2adeb3a655..fc3dfc78dc 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -46,12 +46,6 @@ let atactic n = type entry_name = EntryName : 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name -let try_get_entry u s = - let open Extend in - (** Order the effects: get_entry can raise Not_found *) - let TypedEntry (typ, e) = get_entry u s in - EntryName (typ, Aentry (name_of_entry e)) - (** Quite ad-hoc *) let get_tacentry n m = let open Extend in |