diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 8 | ||||
| -rw-r--r-- | engine/eConstr.mli | 2 | ||||
| -rw-r--r-- | engine/evd.mli | 4 | ||||
| -rw-r--r-- | engine/univSubst.ml | 20 |
4 files changed, 10 insertions, 24 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 diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e914d4f884..0d038e9a67 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -60,7 +60,7 @@ sig val is_empty : t -> bool end -type case_invert = (t, EInstance.t) pcase_invert +type case_invert = t pcase_invert type case = (t, t, EInstance.t) pcase type 'a puniverses = 'a * EInstance.t diff --git a/engine/evd.mli b/engine/evd.mli index ec9ae6fca9..58f635b7bd 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -772,8 +772,8 @@ module MiniEConstr : sig (Constr.t, Constr.types) Context.Named.Declaration.pt val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt - val of_case_invert : (constr,Univ.Instance.t) pcase_invert -> (econstr,EInstance.t) pcase_invert - val unsafe_to_case_invert : (econstr,EInstance.t) pcase_invert -> (constr,Univ.Instance.t) pcase_invert + val of_case_invert : constr pcase_invert -> econstr pcase_invert + val unsafe_to_case_invert : econstr pcase_invert -> constr pcase_invert val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt -> diff --git a/engine/univSubst.ml b/engine/univSubst.ml index e2721b4822..330ed5d0ad 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -68,15 +68,10 @@ let subst_univs_fn_constr f c = let u' = fi u in if u' == u then t else (changed := true; mkConstructU (c, u')) - | Case (ci, u, pms, p, NoInvert, c, br) -> + | Case (ci, u, pms, p, iv, c, br) -> let u' = fi u in if u' == u then map aux t - else (changed := true; map aux (mkCase (ci, u', pms, p, NoInvert, c, br))) - | Case (ci, u, pms, p, CaseInvert{univs;args}, c, br) -> - let u' = fi u in - let univs' = fi univs in - if u' == u && univs' == univs then map aux t - else (changed := true; map aux (mkCase (ci, u', pms, p, CaseInvert {univs = univs'; args}, c, br))) + else (changed := true; map aux (mkCase (ci, u', pms, p, iv, c, br))) | _ -> map aux t in let c' = aux c in @@ -156,15 +151,10 @@ let nf_evars_and_universes_opt_subst f subst = | Sort (Type u) -> let u' = Univ.subst_univs_universe subst u in if u' == u then c else mkSort (sort_of_univ u') - | Case (ci, u, pms, p, NoInvert, t, br) -> - let u' = Instance.subst_fn lsubst u in - if u' == u then map aux c - else Constr.map aux (mkCase (ci, u', pms, p, NoInvert, t, br)) - | Case (ci,u,pms,p,CaseInvert {univs;args},t,br) -> + | Case (ci,u,pms,p,iv,t,br) -> let u' = Instance.subst_fn lsubst u in - let univs' = Instance.subst_fn lsubst univs in - if u' == u && univs' == univs then Constr.map aux c - else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},t,br)) + if u' == u then Constr.map aux c + else Constr.map aux (mkCase (ci,u',pms,p,iv,t,br)) | Array (u,elems,def,ty) -> let u' = Univ.Instance.subst_fn lsubst u in let elems' = CArray.Smart.map aux elems in |