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 /engine/eConstr.ml | |
| parent | b6d5332c6e3127ba3fec466abe502ee40c031ed2 (diff) | |
Remove redundant univ and parameter info from CaseInvert
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 7748df1a9b..157995a173 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -37,7 +37,7 @@ type constr = t type existential = t pexistential type case_return = t pcase_return type case_branch = t pcase_branch -type case_invert = (t, EInstance.t) pcase_invert +type case_invert = t pcase_invert type case = (t, t, EInstance.t) pcase type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint @@ -636,11 +636,7 @@ let universes_of_constr sigma c = | Array (u,_,_,_) -> let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in fold sigma aux s c - | Case (_,u,_,_,CaseInvert {univs;args=_},_,_) -> - let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in - let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma univs)) s in - fold sigma aux s c - | Case (_, u, _, _, NoInvert, _, _) -> + | Case (_,u,_,_,_,_,_) -> let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in fold sigma aux s c | _ -> fold sigma aux s c |