From bb2d7f94ba8688f57dc62ca72a857b82368aa784 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 23 May 2018 18:23:28 +0200 Subject: Moving Option.smart_map to Option.Smart.map. --- pretyping/detyping.ml | 14 +++++++------- pretyping/glob_ops.ml | 2 +- pretyping/patternops.ml | 4 ++-- pretyping/recordops.ml | 2 +- pretyping/typeclasses.ml | 8 ++++---- 5 files changed, 15 insertions(+), 15 deletions(-) (limited to 'pretyping') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index e306fd6b3..779508477 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -957,17 +957,17 @@ let rec subst_glob_constr subst = DAst.map (function | GLetIn (n,r1,t,r2) as raw -> let r1' = subst_glob_constr subst r1 in let r2' = subst_glob_constr subst r2 in - let t' = Option.smartmap (subst_glob_constr subst) t in + let t' = Option.Smart.map (subst_glob_constr subst) t in if r1' == r1 && t == t' && r2' == r2 then raw else GLetIn (n,r1',t',r2') | GCases (sty,rtno,rl,branches) as raw -> let open CAst in - let rtno' = Option.smartmap (subst_glob_constr subst) rtno + let rtno' = Option.Smart.map (subst_glob_constr subst) rtno and rl' = List.Smart.map (fun (a,x as y) -> let a' = subst_glob_constr subst a in let (n,topt) = x in - let topt' = Option.smartmap + let topt' = Option.Smart.map (fun ({loc;v=((sp,i),y)} as t) -> let sp' = subst_mind subst sp in if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in @@ -985,14 +985,14 @@ let rec subst_glob_constr subst = DAst.map (function GCases (sty,rtno',rl',branches') | GLetTuple (nal,(na,po),b,c) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b' = subst_glob_constr subst b and c' = subst_glob_constr subst c in if po' == po && b' == b && c' == c then raw else GLetTuple (nal,(na,po'),b',c') | GIf (c,(na,po),b1,b2) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b1' = subst_glob_constr subst b1 and b2' = subst_glob_constr subst b2 and c' = subst_glob_constr subst c in @@ -1005,7 +1005,7 @@ let rec subst_glob_constr subst = DAst.map (function let bl' = Array.Smart.map (List.Smart.map (fun (na,k,obd,ty as dcl) -> let ty' = subst_glob_constr subst ty in - let obd' = Option.smartmap (subst_glob_constr subst) obd in + let obd' = Option.Smart.map (subst_glob_constr subst) obd in if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else @@ -1018,7 +1018,7 @@ let rec subst_glob_constr subst = DAst.map (function if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in + let nsolve = Option.Smart.map (Hook.get f_subst_genarg subst) solve in if nsolve == solve && nknd == knd then raw else GHole (nknd, naming, nsolve) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 102e89400..5056c0457 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -343,7 +343,7 @@ let map_inpattern_binders f ({loc;v=(id,nal)} as x) = else CAst.make ?loc (id,r) let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = - let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in + let r = Option.Smart.map (fun p -> map_inpattern_binders f p) inp in if r == inp then x else c,(f na, r) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b425dc0e2..375ed10d0 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -312,7 +312,7 @@ let rec subst_pattern subst pat = PProd (name,c1',c2') | PLetIn (name,c1,t,c2) -> let c1' = subst_pattern subst c1 in - let t' = Option.smartmap (subst_pattern subst) t in + let t' = Option.Smart.map (subst_pattern subst) t in let c2' = subst_pattern subst c2 in if c1' == c1 && t' == t && c2' == c2 then pat else PLetIn (name,c1',t',c2') @@ -326,7 +326,7 @@ let rec subst_pattern subst pat = PIf (c',c1',c2') | PCase (cip,typ,c,branches) -> let ind = cip.cip_ind in - let ind' = Option.smartmap (subst_ind subst) ind in + let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in let typ' = subst_pattern subst typ in let c' = subst_pattern subst c in diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 334bfc895..9eb410f06 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -70,7 +70,7 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) List.Smart.map - (Option.smartmap (fun kn -> fst (subst_con_kn subst kn))) + (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn))) projs in let id' = fst (subst_constructor subst id) in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 5ad9dc691..12a944d32 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -182,10 +182,10 @@ let subst_class (subst,cl) = and do_subst_gr gr = fst (subst_global subst gr) in let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.Smart.map (Option.smartmap do_subst_gr) grs, + List.Smart.map (Option.Smart.map do_subst_gr) grs, do_subst_ctx ctx in let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> - (x, y, Option.smartmap do_subst_con z)) projs in + (x, y, Option.Smart.map do_subst_con z)) projs in { cl_univs = cl.cl_univs; cl_impl = do_subst_gr cl.cl_impl; cl_context = do_subst_context cl.cl_context; @@ -223,7 +223,7 @@ let discharge_class (_,cl) = | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.Smart.map (Option.smartmap Lib.discharge_global) grs + List.Smart.map (Option.Smart.map Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in @@ -234,7 +234,7 @@ let discharge_class (_,cl) = let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in - let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in + let discharge_proj (x, y, z) = x, y, Option.Smart.map Lib.discharge_con z in { cl_univs = cl_univs'; cl_impl = cl_impl'; cl_context = context; -- cgit v1.2.3