diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/ground.ml | 16 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 14 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 8 |
3 files changed, 17 insertions, 21 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 4e3ba57308..516b04ea21 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -13,23 +13,21 @@ open Formula open Sequent open Rules open Instances -open Constr open Tacmach.New open Tacticals.New +open Globnames let update_flags ()= - let predref=ref Names.Cpred.empty in - let f coe= - try - let kn= fst (destConst (Classops.get_coercion_value coe)) in - predref:=Names.Cpred.add kn !predref - with DestKO -> () + let f acc coe = + match coe.Classops.coe_value with + | ConstRef c -> Names.Cpred.add c acc + | _ -> acc in - List.iter f (Classops.coercions ()); + let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in red_flags:= CClosure.RedFlags.red_add_transparent CClosure.betaiotazeta - (Names.Id.Pred.full,Names.Cpred.complement !predref) + (Names.Id.Pred.full,Names.Cpred.complement pred) let ground_tac solver startseq = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 7ce2dd64af..989a6c5bf1 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -24,7 +24,6 @@ open Ltac_plugin open Notation_ops open Notation_term open Glob_term -open Globnames open Stdarg open Genarg open Decl_kinds @@ -218,8 +217,8 @@ let interp_search_notation ?loc tag okey = (Bytes.set s' i' '_'; loop (j + 1) (i' + 2)) else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in loop 0 1 in - let trim_ntn (pntn, m) = Bytes.sub_string pntn 1 (max 0 m) in - let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in + let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in + let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in let pr_and_list pr = function | [x] -> pr x | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x @@ -294,7 +293,7 @@ let interp_search_notation ?loc tag okey = let scs' = List.remove (=) sc !scs in let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in Feedback.msg_warning (hov 4 w) - else if String.string_contains ~where:ntn ~what:" .. " then + else if String.string_contains ~where:(snd ntn) ~what:" .. " then err (pr_ntn ntn ++ str " is an n-ary notation"); let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in let rec sub () = function @@ -359,13 +358,12 @@ let coerce_search_pattern_to_sort hpat = true, cp with _ -> false, [] in let coerce hp coe_index = - let coe = Classops.get_coercion_value coe_index in + let coe_ref = coe_index.Classops.coe_value in try - let coe_ref = global_of_constr coe in let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] - with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () + with Not_found | Option.IsNone -> + errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 05eda14e90..30a998c6ce 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -929,7 +929,7 @@ let glob_cpattern gs p = | k, (v, Some t), _ as orig -> if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else match t.CAst.v with - | CNotation("( _ in _ )", ([t1; t2], [], [], [])) -> + | CNotation((InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] | (r1, Some _), (r2, Some _) when isCVar t1 -> @@ -937,11 +937,11 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] | _ -> CErrors.anomaly (str"where are we?.") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [], [])) -> + | CNotation((InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation("( _ as _ )", ([t1; t2], [], [], [])) -> + | CNotation((InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) -> encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [], [])) -> + | CNotation((InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] | _ -> glob_ssrterm gs orig ;; |