diff options
| author | Gaëtan Gilbert | 2019-06-13 15:39:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 13:06:22 +0200 |
| commit | 2ded4c25e532c5dfca0483c211653768ebed01a7 (patch) | |
| tree | a04b2f787490c8971590e6bdf7dd1ec4220e0290 /kernel/vars.ml | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index a4465c293b..63d88c659a 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -252,6 +252,12 @@ let subst_univs_level_constr subst c = let u' = Univ.subst_univs_level_universe subst u in 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 + 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))) | _ -> Constr.map aux t in let c' = aux c in @@ -288,6 +294,10 @@ let subst_instance_constr subst c = let u' = Univ.subst_instance_universe subst u in 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)) | _ -> Constr.map aux t in aux c |