diff options
Diffstat (limited to 'plugins/ssrmatching/ssrmatching.ml4')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 814e3a4d5..ff1db8cf5 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -61,8 +61,8 @@ DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = Errors.errorlabstrm "ssrmatching" -let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg) +let errorstrm = CErrors.errorlabstrm "ssrmatching" +let loc_error loc msg = CErrors.user_err_loc (loc, msg, str msg) let ppnl = Feedback.msg_info (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) @@ -89,7 +89,7 @@ let env_size env = List.length (Environ.named_context env) let safeDestApp c = match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |] let get_index = function ArgArg i -> i | _ -> - Errors.anomaly (str"Uninterpreted index") + CErrors.anomaly (str"Uninterpreted index") (* Toplevel constr must be globalized twice ! *) let glob_constr ist genv = function | _, Some ce -> @@ -150,7 +150,7 @@ let dC t = CastConv t (** Constructors for constr_expr *) let isCVar = function CRef (Ident _, _) -> true | _ -> false let destCVar = function CRef (Ident (_, id), _) -> id | _ -> - Errors.anomaly (str"not a CRef") + CErrors.anomaly (str"not a CRef") let mkCHole loc = CHole (loc, None, IntroAnonymous, None) let mkCLambda loc name ty t = CLambdaN (loc, [[loc, name], Default Explicit, ty], t) @@ -167,8 +167,8 @@ let mkRLambda n s t = GLambda (dummy_loc, n, Explicit, s, t) let combineCG t1 t2 f g = match t1, t2 with | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) | (x, (_, Some t1)), (_, (_, Some t2)) -> x, (mkRHole, Some (f t1 t2)) - | _, (_, (_, None)) -> Errors.anomaly (str"have: mixed C-G constr") - | _ -> Errors.anomaly (str"have: mixed G-C constr") + | _, (_, (_, None)) -> CErrors.anomaly (str"have: mixed C-G constr") + | _ -> CErrors.anomaly (str"have: mixed G-C constr") let loc_ofCG = function | (_, (s, None)) -> Glob_ops.loc_of_glob_constr s | (_, (_, Some s)) -> Constrexpr_ops.constr_loc s @@ -491,7 +491,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = | Evar (k, _) -> if Evd.mem sigma0 k then KpatEvar k, f, a else if a <> [] then KpatFlex, f, a else - (match p_origin with None -> Errors.error "indeterminate pattern" + (match p_origin with None -> CErrors.error "indeterminate pattern" | Some (dir, rule) -> errorstrm (str "indeterminate " ++ pr_dir_side dir ++ str " in " ++ pr_constr_pat rule)) @@ -632,12 +632,12 @@ let match_upats_FO upats env sigma0 ise orig_c = let pt' = unif_end env sigma0 ise' u.up_t (u.up_ok lhs) in raise (FoundUnif (ungen_upat lhs pt' u)) with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u - | Not_found -> Errors.anomaly (str"incomplete ise in match_upats_FO") + | Not_found -> CErrors.anomaly (str"incomplete ise in match_upats_FO") | _ -> () in List.iter one_match fpats done; iter_constr_LR loop f; Array.iter loop a in - try loop orig_c with Invalid_argument _ -> Errors.anomaly (str"IN FO") + try loop orig_c with Invalid_argument _ -> CErrors.anomaly (str"IN FO") let prof_FO = mk_profiler "match_upats_FO";; let match_upats_FO upats env sigma0 ise c = @@ -684,7 +684,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsatisfiableConstraints _) -> failed_because_of_TC:=true - | e when Errors.noncritical e -> () in + | e when CErrors.noncritical e -> () in List.iter one_match fpats done; iter_constr_LR (aux upats env sigma0 ise) f; @@ -707,11 +707,11 @@ let fixed_upat = function let do_once r f = match !r with Some _ -> () | None -> r := Some (f ()) let assert_done r = - match !r with Some x -> x | None -> Errors.anomaly (str"do_once never called") + match !r with Some x -> x | None -> CErrors.anomaly (str"do_once never called") let assert_done_multires r = match !r with - | None -> Errors.anomaly (str"do_once never called") + | None -> CErrors.anomaly (str"do_once never called") | Some (n, xs) -> r := Some (n+1,xs); try List.nth xs n with Failure _ -> raise NoMatch @@ -768,7 +768,7 @@ let source () = match upats_origin, upats with | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ pr_constr_pat rule ++ spc() | _, [] | None, _::_::_ -> - Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in + CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin") in let on_instance, instances = let instances = ref [] in (fun x -> @@ -806,7 +806,7 @@ let rec uniquize = function errorstrm (source () ++ str "does not match any subterm of the goal") | NoProgress when (not raise_NoMatch) -> let dir = match upats_origin with Some (d,_) -> d | _ -> - Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in + CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin") in errorstrm (str"all matches of "++source()++ str"are equal to the " ++ pr_dir_side (inv_dir dir)) | NoProgress -> raise NoMatch); @@ -841,7 +841,7 @@ let rec uniquize = function let sigma, uc, ({up_f = pf; up_a = pa} as u) = match !upat_that_matched with | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch - | None -> Errors.anomaly (str"companion function never called") in + | None -> CErrors.anomaly (str"companion function never called") in let p' = mkApp (pf, pa) in if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t) else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++ @@ -1022,7 +1022,7 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) when isCVar t1 -> encode k "In" [r1; r2; bind_in t1 t2] | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] - | _ -> Errors.anomaly (str"where are we?") + | _ -> CErrors.anomaly (str"where are we?") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] @@ -1109,9 +1109,9 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let v = Id.Map.find id ist.lfun in Option.get reccall (Value.cast (topwit (Option.get wit_ssrpatternarg)) v) - | it -> g t with e when Errors.noncritical e -> g t in + | it -> g t with e when CErrors.noncritical e -> g t in let decodeG t f g = decode ist (mkG t) f g in - let bad_enc id _ = Errors.anomaly (str"bad encoding for pattern "++str id) in + let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id) in let cleanup_XinE h x rp sigma = let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in let to_clean, update = (* handle rename if x is already used *) @@ -1297,7 +1297,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = let e = match p with - | In_T _ | In_X_In_T _ -> Errors.anomaly (str"pattern without redex") + | In_T _ | In_X_In_T _ -> CErrors.anomaly (str"pattern without redex") | T e | X_In_T (e, _) | E_As_X_In_T (e, _, _) | E_In_X_In_T (e, _, _) -> e in let sigma = if not resolve_typeclasses then sigma @@ -1335,7 +1335,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let fill_occ_term env cl occ sigma0 (sigma, t) = try let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in - if sigma' != sigma0 then Errors.error "matching impacts evars" + if sigma' != sigma0 then CErrors.error "matching impacts evars" else cl, (Evd.merge_universe_context sigma' uc, t') with NoMatch -> try let sigma', uc, t' = |