diff options
Diffstat (limited to 'checker/term.ml')
| -rw-r--r-- | checker/term.ml | 42 |
1 files changed, 30 insertions, 12 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 |