diff options
Diffstat (limited to 'contrib/interface/xlate.ml')
| -rw-r--r-- | contrib/interface/xlate.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 02f36a8c8..ee48ee53b 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1958,12 +1958,14 @@ let rec xlate_vernac = let xlate_search_about_item (b,it) = if not b then xlate_error "TODO: negative searchabout constraint"; match it with - SearchRef x -> + SearchSubPattern (CRef x) -> CT_coerce_ID_to_ID_OR_STRING(loc_qualid_to_ct_ID x) | SearchString (s,None) -> CT_coerce_STRING_to_ID_OR_STRING(CT_string s) - | SearchString (s,_) -> - xlate_error "TODO: notation with explicit scope" in + | SearchString _ | SearchSubPattern _ -> + xlate_error + "TODO: search subpatterns or notation with explicit scope" + in CT_search_about (CT_id_or_string_ne_list(xlate_search_about_item a, List.map xlate_search_about_item l), |