diff options
Diffstat (limited to 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 38 |
1 files changed, 27 insertions, 11 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index a446fa413c..b09577d4db 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -253,12 +253,20 @@ let subst_univs_level_constr subst c = if u' == u then t else (changed := true; mkSort (Sorts.sort_of_univ u')) - | Case (ci,p,CaseInvert {univs;args},c,br) -> - if Univ.Instance.is_empty univs then Constr.map aux t + | Case (ci, u, pms, p, CaseInvert {indices}, c, br) -> + if Univ.Instance.is_empty u then Constr.map aux t else - let univs' = f univs in - if univs' == univs then Constr.map aux t - else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))) + let u' = f u in + if u' == u then Constr.map aux t + else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},c,br))) + + | Case (ci, u, pms, p, NoInvert, c, br) -> + if Univ.Instance.is_empty u then Constr.map aux t + else + let u' = f u in + if u' == u then Constr.map aux t + else + (changed := true; Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br))) | Array (u,elems,def,ty) -> let u' = f u in @@ -305,10 +313,18 @@ let subst_instance_constr subst c = if u' == u then t else (mkSort (Sorts.sort_of_univ u')) - | Case (ci,p,CaseInvert {univs;args},c,br) -> - let univs' = f univs in - if univs' == univs then Constr.map aux t - else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)) + | Case (ci, u, pms, p, CaseInvert {indices}, c, br) -> + let u' = f u in + if u' == u then Constr.map aux t + else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},c,br)) + + | Case (ci, u, pms, p, NoInvert, c, br) -> + if Univ.Instance.is_empty u then Constr.map aux t + else + let u' = f u in + if u' == u then Constr.map aux t + else + Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br)) | Array (u,elems,def,ty) -> let u' = f u in @@ -348,8 +364,8 @@ let universes_of_constr c = | Array (u,_,_,_) -> let s = LSet.fold LSet.add (Instance.levels u) s in Constr.fold aux s c - | Case (_,_,CaseInvert {univs;args=_},_,_) -> - let s = LSet.fold LSet.add (Instance.levels univs) s in + | Case (_, u, _, _, _,_ ,_) -> + let s = LSet.fold LSet.add (Instance.levels u) s in Constr.fold aux s c | _ -> Constr.fold aux s c in aux LSet.empty c |