diff options
| author | Gaëtan Gilbert | 2020-12-11 13:20:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:02:02 +0100 |
| commit | 868b948f8a7bd583d467c5d02dfb34d328d53d37 (patch) | |
| tree | 045e0b730c5abebafe6300fa382b71034519a024 /kernel/vars.ml | |
| parent | b6d5332c6e3127ba3fec466abe502ee40c031ed2 (diff) | |
Remove redundant univ and parameter info from CaseInvert
Diffstat (limited to 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 21 |
1 files changed, 8 insertions, 13 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index 0f71057787..b09577d4db 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -253,13 +253,12 @@ let subst_univs_level_constr subst c = if u' == u then t else (changed := true; mkSort (Sorts.sort_of_univ u')) - | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) -> - if Univ.Instance.is_empty u && 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 u' = f u in - let univs' = f univs in - if u' == u && univs' == univs then Constr.map aux t - else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br))) + 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 @@ -314,11 +313,10 @@ let subst_instance_constr subst c = if u' == u then t else (mkSort (Sorts.sort_of_univ u')) - | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) -> + | Case (ci, u, pms, p, CaseInvert {indices}, c, br) -> let u' = f u in - let univs' = f univs in - if u' == u && univs' == univs then Constr.map aux t - else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br)) + 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 @@ -366,11 +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 (_, u, _, _, CaseInvert {univs;args=_},_ ,_) -> + | Case (_, u, _, _, _,_ ,_) -> let s = LSet.fold LSet.add (Instance.levels u) s in - let s = LSet.fold LSet.add (Instance.levels univs) s in Constr.fold aux s c - | Case (_, u, _, _, NoInvert, _, _) -> - Constr.fold aux (LSet.fold LSet.add (Instance.levels u) s) c | _ -> Constr.fold aux s c in aux LSet.empty c |