aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--checker/term.ml42
-rw-r--r--kernel/vars.ml42
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;; *)