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 /pretyping/detyping.ml | |
| parent | 33b5074f24270c202a9922f21d445c12cc6b3b3d (diff) | |
Moving Option.smart_map to Option.Smart.map.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 14 |
1 files changed, 7 insertions, 7 deletions
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) |