diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ea2889dea..e306fd6b3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -920,7 +920,7 @@ let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_cases_pattern subst) cpl in + and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (((kn',i),j),cpl',n) ) @@ -940,7 +940,7 @@ let rec subst_glob_constr subst = DAst.map (function | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r - and rl' = List.smartmap (subst_glob_constr subst) rl in + and rl' = List.Smart.map (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') @@ -964,7 +964,7 @@ let rec subst_glob_constr subst = DAst.map (function | GCases (sty,rtno,rl,branches) as raw -> let open CAst in let rtno' = Option.smartmap (subst_glob_constr subst) rtno - and rl' = List.smartmap (fun (a,x as y) -> + 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 @@ -972,10 +972,10 @@ let rec subst_glob_constr subst = DAst.map (function let sp' = subst_mind subst sp in if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = - List.smartmap (subst_cases_pattern subst) cpl + List.Smart.map (subst_cases_pattern subst) cpl and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) @@ -1003,7 +1003,7 @@ let rec subst_glob_constr subst = DAst.map (function let ra1' = Array.Smart.map (subst_glob_constr subst) ra1 and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in let bl' = Array.Smart.map - (List.smartmap (fun (na,k,obd,ty as dcl) -> + (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 if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) |