diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-23 13:34:46 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-23 18:50:10 +0200 |
commit | 33b5074f24270c202a9922f21d445c12cc6b3b3d (patch) | |
tree | 67d69b51caf3b7849e2d90d21e6ed7dc705d3249 /pretyping/typeclasses.ml | |
parent | 944f62d08b7d78bcb20dd12ba138891d432b5987 (diff) |
Collecting List.smart_* functions into a module List.Smart.
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r-- | pretyping/typeclasses.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 11cc6c1f0..5ad9dc691 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -180,11 +180,11 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in + let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap do_subst_gr) grs, + List.Smart.map (Option.smartmap do_subst_gr) grs, do_subst_ctx ctx in - let do_subst_projs projs = List.smartmap (fun (x, y, z) -> + let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in { cl_univs = cl.cl_univs; cl_impl = do_subst_gr cl.cl_impl; @@ -223,7 +223,7 @@ let discharge_class (_,cl) = | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap Lib.discharge_global) grs + List.Smart.map (Option.smartmap 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 @@ -239,7 +239,7 @@ let discharge_class (_,cl) = cl_impl = cl_impl'; cl_context = context; cl_props = props; - cl_projs = List.smartmap discharge_proj cl.cl_projs; + cl_projs = List.Smart.map discharge_proj cl.cl_projs; cl_strict = cl.cl_strict; cl_unique = cl.cl_unique } |