diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-23 18:23:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-23 18:50:10 +0200 |
| commit | bb2d7f94ba8688f57dc62ca72a857b82368aa784 (patch) | |
| tree | 5282ed7a0038ce0babbfc1b8b94eefa870707be8 /kernel | |
| parent | 33b5074f24270c202a9922f21d445c12cc6b3b3d (diff) | |
Moving Option.smart_map to Option.Smart.map.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declareops.ml | 6 | ||||
| -rw-r--r-- | kernel/modops.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index f2f43144e..cc0b381c9 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -42,7 +42,7 @@ let map_decl_arity f g = function let hcons_template_arity ar = { template_param_levels = ar.template_param_levels; - (* List.Smart.map (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *) + (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) template_level = Univ.hcons_univ ar.template_level } (** {6 Constants } *) @@ -94,7 +94,7 @@ let subst_const_body sub cb = else let body' = subst_const_def sub cb.const_body in let type' = subst_const_type sub cb.const_type in - let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in + let proj' = Option.Smart.map (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type && proj' == cb.const_proj then cb else @@ -217,7 +217,7 @@ let subst_mind_record sub (id, ps, pb as r) = else (id, ps', pb') let subst_mind_body sub mib = - { mind_record = Option.smartmap (Option.smartmap (subst_mind_record sub)) mib.mind_record ; + { mind_record = Option.Smart.map (Option.Smart.map (subst_mind_record sub)) mib.mind_record ; mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); diff --git a/kernel/modops.ml b/kernel/modops.ml index daee0f187..58ebb4ad7 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -210,7 +210,7 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> in let ty' = subst_signature sub do_delta ty in let me' = subst_impl sub me in - let aty' = Option.smartmap (subst_expression sub id_delta) aty in + let aty' = Option.Smart.map (subst_expression sub id_delta) aty in let delta' = do_delta mb.mod_delta sub in if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta then mb |