diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml4 | 16 | ||||
| -rw-r--r-- | contrib/interface/dad.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 8 |
3 files changed, 15 insertions, 11 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index e7c7fde8dd..51dce4f766 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -545,7 +545,9 @@ let solve_hook n = let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s) let interp_search_about_item = function - | SearchRef qid -> GlobSearchRef (Nametab.global qid) + | SearchSubPattern pat -> + let _,pat = Constrintern.intern_constr_pattern Evd.empty (Global.env()) pat in + GlobSearchSubPattern pat | SearchString (s,_) -> warning "Notation case not taken into account"; GlobSearchString s @@ -563,10 +565,10 @@ let pcoq_search s l = raw_search_about (filter_by_module_from_list l) add_search (List.map (on_snd interp_search_about_item) sl) | SearchPattern c -> - let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in raw_pattern_search (filter_by_module_from_list l) add_search pat | SearchRewrite c -> - let _,pat = interp_constrpattern Evd.empty (Global.env()) c in + let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in raw_search_rewrite (filter_by_module_from_list l) add_search pat; | SearchHead locqid -> filtered_search @@ -581,7 +583,7 @@ let rec hyp_pattern_filter pat name a c = | Prod(_, hyp, c2) -> (try (* let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in - let _ = msgnl ((str "PAT ") ++ (Printer.pr_pattern pat)) in *) + let _ = msgnl ((str "PAT ") ++ (Printer.pr_constr_pattern pat)) in *) if Matching.is_matching pat hyp then (msgnl (str "ok"); true) else @@ -591,7 +593,7 @@ let rec hyp_pattern_filter pat name a c = | _ -> false;; let hyp_search_pattern c l = - let _, pat = interp_constrpattern Evd.empty (Global.env()) c in + let _, pat = intern_constr_pattern Evd.empty (Global.env()) c in ctv_SEARCH_LIST := []; gen_filtered_search (fun s a c -> (filter_by_module_from_list l s a c && @@ -640,8 +642,8 @@ let pcoq_term_pr = { * Except with right bool/env which I'll get :) *) pr_lconstr_expr = (fun c -> fFORMULA (xlate_formula c) ++ str "(pcoq_lconstr_expr of " ++ (default_term_pr.pr_lconstr_expr c) ++ str ")"); - pr_pattern_expr = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_pattern_expr c)); - pr_lpattern_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_lpattern_expr c)) + pr_constr_pattern_expr = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_constr_pattern_expr c)); + pr_lconstr_pattern_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_lconstr_pattern_expr c)) } let start_pcoq_trees () = diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml index 8096bc3111..c2ab2dc8d0 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -99,7 +99,7 @@ let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 = with Failure s -> failwith "internal" in let _, constr_pat = - interp_constrpattern Evd.empty (Global.env()) + intern_constr_pattern Evd.empty (Global.env()) ((*ct_to_ast*) pat) in let subst = matches constr_pat term_to_match in if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 02f36a8c88..ee48ee53b7 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), |