diff options
| -rw-r--r-- | checker/term.ml | 42 | ||||
| -rw-r--r-- | kernel/vars.ml | 42 |
2 files changed, 60 insertions, 24 deletions
diff --git a/checker/term.ml b/checker/term.ml index c0f8e0106..dea3d3e65 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -413,18 +413,36 @@ let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c let subst_instance_constr subst c = - let f u = Univ.subst_instance_instance subst u in - let rec aux t = - match t with - | Const (c, u) -> Const (c, f u) - | Ind (i, u) -> Ind (i, f u) - | Construct (c, u) -> Construct (c, f u) - | Sort (Type u) -> - let u' = Univ.subst_instance_universe subst u in - Sort (sort_of_univ u') - | _ -> map_constr aux t - in - aux c + if Univ.Instance.is_empty subst then c + else + let f u = Univ.subst_instance_instance subst u in + let rec aux t = + match t with + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (Const (c, u')) + | Ind (i, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (Ind (i, u')) + | Construct (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (Construct (c, u')) + | Sort (Type u) -> + let u' = Univ.subst_instance_universe subst u in + if u' == u then t else + (Sort (sort_of_univ u')) + | _ -> map_constr aux t + in + aux c let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx diff --git a/kernel/vars.ml b/kernel/vars.ml index 89c17b850..baf8fa31f 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -316,18 +316,36 @@ let subst_univs_level_context s = Context.Rel.map (subst_univs_level_constr s) let subst_instance_constr subst c = - let f u = Univ.subst_instance_instance subst u in - let rec aux t = - match kind t with - | Const (c, u) -> mkConstU (c, f u) - | Ind (i, u) -> mkIndU (i, f u) - | Construct (c, u) -> mkConstructU (c, f u) - | Sort (Sorts.Type u) -> - let u' = Univ.subst_instance_universe subst u in - mkSort (Sorts.sort_of_univ u') - | _ -> Constr.map aux t - in - aux c + if Univ.Instance.is_empty subst then c + else + let f u = Univ.subst_instance_instance subst u in + let rec aux t = + match kind t with + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkConstU (c, u')) + | Ind (i, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkIndU (i, u')) + | Construct (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (mkConstructU (c, u')) + | Sort (Sorts.Type u) -> + let u' = Univ.subst_instance_universe subst u in + if u' == u then t else + (mkSort (Sorts.sort_of_univ u')) + | _ -> Constr.map aux t + in + aux c (* let substkey = Profile.declare_profile "subst_instance_constr";; *) (* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) |