From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Mon, 29 May 2017 11:02:06 +0200 Subject: Remove (useless) aliases from the API. --- plugins/ssrmatching/ssrmatching.ml4 | 20 ++++++++++---------- plugins/ssrmatching/ssrmatching.mli | 10 +++++----- 2 files changed, 15 insertions(+), 15 deletions(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 051a9fb4e..796b6f43e 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -400,7 +400,7 @@ type pattern_class = | KpatLam | KpatRigid | KpatFlex - | KpatProj of constant + | KpatProj of Constant.t type tpattern = { up_k : pattern_class; @@ -421,7 +421,7 @@ let isRigid c = match kind_of_term c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true | _ -> false -let hole_var = mkVar (id_of_string "_") +let hole_var = mkVar (Id.of_string "_") let pr_constr_pat c0 = let rec wipe_evar c = if isEvar c then hole_var else map_constr wipe_evar c in @@ -448,7 +448,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = Context.Named.fold_inside abs_dc ~init:([], (put evi.evar_concl)) dc in let m = Evarutil.new_meta () in ise := meta_declare m t !ise; - sigma := Evd.define k (applist (mkMeta m, a)) !sigma; + sigma := Evd.define k (applistc (mkMeta m) a) !sigma; put (existential_value !sigma ex) end | _ -> map_constr put c in @@ -465,7 +465,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = | Const (p,_) -> let np = proj_nparams p in if np = 0 || np > List.length a then KpatConst, f, a else - let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2 + let a1, a2 = List.chop np a in KpatProj p, (applistc f a1), a2 | Proj (p,arg) -> KpatProj (Projection.constant p), f, a | Var _ | Ind _ | Construct _ -> KpatFixed, f, a | Evar (k, _) -> @@ -571,7 +571,7 @@ let filter_upat_FO i0 f n u fpats = | KpatFlex -> i0 := n; true in if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats -exception FoundUnif of (evar_map * evar_universe_context * tpattern) +exception FoundUnif of (evar_map * UState.t * tpattern) (* Note: we don't update env as we descend into the term, as the primitive *) (* unification procedure always rejects subterms with bound variables. *) @@ -714,7 +714,7 @@ type find_P = k:subst -> constr type conclude = unit -> - constr * ssrdir * (Evd.evar_map * Evd.evar_universe_context * constr) + constr * ssrdir * (Evd.evar_map * UState.t * constr) (* upats_origin makes a better error message only *) let mk_tpattern_matcher ?(all_instances=false) @@ -905,7 +905,7 @@ let glob_cpattern gs p = pp(lazy(str"globbing pattern: " ++ pr_term p)); let glob x = snd (glob_ssrterm gs (mk_lterm x)) in let encode k s l = - let name = Name (id_of_string ("_ssrpat_" ^ s)) in + let name = Name (Id.of_string ("_ssrpat_" ^ s)) in k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in let bind_in t1 t2 = let mkCHole = mkCHole ~loc:None in let n = Name (destCVar t1) in @@ -1131,9 +1131,9 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = sigma in let red = let rec decode_red (ist,red) = let open CAst in match red with | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None)) - when let id = string_of_id id in let len = String.length id in + when let id = Id.to_string id in let len = String.length id in (len > 8 && String.sub id 0 8 = "_ssrpat_") -> - let id = string_of_id id in let len = String.length id in + let id = Id.to_string id in let len = String.length id in (match String.sub id 8 (len - 8), t with | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x) | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id) @@ -1377,7 +1377,7 @@ let ssrpatterntac _ist (arg_ist,arg) gl = let t = EConstr.of_constr t in let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in - let concl = EConstr.mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in + let concl = EConstr.mkLetIn (Name (Id.of_string "selected"), t, tty, concl_x) in Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 088dd021e..c2bf12cb6 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -154,7 +154,7 @@ type find_P = instantiation, the proof term and the ssrdit stored in the tpattern @raise UserEerror if too many occurrences were specified *) type conclude = - unit -> constr * ssrdir * (evar_map * Evd.evar_universe_context * constr) + unit -> constr * ssrdir * (evar_map * UState.t * constr) (** [mk_tpattern_matcher b o sigma0 occ sigma_tplist] creates a pair a function [find_P] and [conclude] with the behaviour explained above. @@ -224,12 +224,12 @@ val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma on top of the former APIs *) val tag_of_cpattern : cpattern -> char val loc_of_cpattern : cpattern -> Loc.t option -val id_of_pattern : pattern -> Names.variable option +val id_of_pattern : pattern -> Names.Id.t option val is_wildcard : cpattern -> bool -val cpattern_of_id : Names.variable -> cpattern +val cpattern_of_id : Names.Id.t -> cpattern val pr_constr_pat : constr -> Pp.std_ppcmds -val pf_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma -val pf_unsafe_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma +val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma +val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma (* One can also "Set SsrMatchingDebug" from a .v *) val debug : bool -> unit -- cgit v1.2.3