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 /interp | |
| parent | 33b5074f24270c202a9922f21d445c12cc6b3b3d (diff) | |
Moving Option.smart_map to Option.Smart.map.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation_ops.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index eeda607e6..e51c69136 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -566,13 +566,13 @@ let rec subst_notation_constr subst bound raw = | NLetIn (n,r1,t,r2) -> let r1' = subst_notation_constr subst bound r1 in - let t' = Option.smartmap (subst_notation_constr subst bound) t in + let t' = Option.Smart.map (subst_notation_constr subst bound) t in let r2' = subst_notation_constr subst bound r2 in if r1' == r1 && t == t' && r2' == r2 then raw else NLetIn (n,r1',t',r2') | NCases (sty,rtntypopt,rl,branches) -> - let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt + let rtntypopt' = Option.Smart.map (subst_notation_constr subst bound) rtntypopt and rl' = List.Smart.map (fun (a,(n,signopt) as x) -> let a' = subst_notation_constr subst bound a in @@ -594,14 +594,14 @@ let rec subst_notation_constr subst bound raw = NCases (sty,rtntypopt',rl',branches') | NLetTuple (nal,(na,po),b,c) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po + let po' = Option.Smart.map (subst_notation_constr subst bound) po and b' = subst_notation_constr subst bound b and c' = subst_notation_constr subst bound c in if po' == po && b' == b && c' == c then raw else NLetTuple (nal,(na,po'),b',c') | NIf (c,(na,po),b1,b2) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po + let po' = Option.Smart.map (subst_notation_constr subst bound) po and b1' = subst_notation_constr subst bound b1 and b2' = subst_notation_constr subst bound b2 and c' = subst_notation_constr subst bound c in @@ -611,7 +611,7 @@ let rec subst_notation_constr subst bound raw = | NRec (fk,idl,dll,tl,bl) -> let dll' = Array.Smart.map (List.Smart.map (fun (na,oc,b as x) -> - let oc' = Option.smartmap (subst_notation_constr subst bound) oc in + let oc' = Option.Smart.map (subst_notation_constr subst bound) oc in let b' = subst_notation_constr subst bound b in if oc' == oc && b' == b then x else (na,oc',b'))) dll in let tl' = Array.Smart.map (subst_notation_constr subst bound) tl in @@ -628,7 +628,7 @@ let rec subst_notation_constr subst bound raw = if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in + let nsolve = Option.Smart.map (Genintern.generic_substitute subst) solve in if nsolve == solve && nknd == knd then raw else NHole (nknd, naming, nsolve) |