diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2env.ml')
| -rw-r--r-- | user-contrib/Ltac2/tac2env.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml index 5f9dc3798a..b0a910f10e 100644 --- a/user-contrib/Ltac2/tac2env.ml +++ b/user-contrib/Ltac2/tac2env.ml @@ -196,6 +196,11 @@ let shortest_qualid_of_constructor kn = let sp = KNmap.find kn tab.tab_cstr_rev in KnTab.shortest_qualid Id.Set.empty sp tab.tab_cstr +let mem_constructor qid = + let tab = !nametab in + try ignore (KnTab.locate qid tab.tab_cstr) ; true + with Not_found -> false + let push_type vis sp kn = let tab = !nametab in let tab_type = KnTab.push vis sp kn tab.tab_type in |