diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-06-01 17:05:52 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:19 +0200 |
| commit | 49e4acab949da9861adcd37b8511a89c221ae129 (patch) | |
| tree | 65d38a897d51e3b455e50ac2f30c3c023b7b5a98 /kernel/vars.ml | |
| parent | ff918e4bb0ae23566e038f4b55d84dd2c343f95e (diff) | |
Use a smart map_constr
Diffstat (limited to 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 44 |
1 files changed, 12 insertions, 32 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index 629de80f7..89c17b850 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -316,38 +316,18 @@ let subst_univs_level_context s = Context.Rel.map (subst_univs_level_constr s) let subst_instance_constr subst c = - if Univ.Instance.is_empty subst then c - else - let f u = Univ.subst_instance_instance subst u in - let changed = ref false 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 (changed := true; 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 (changed := true; 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 (changed := true; mkConstructU (c, u')) - | Sort (Sorts.Type u) -> - let u' = Univ.subst_instance_universe subst u in - if u' == u then t else - (changed := true; mkSort (Sorts.sort_of_univ u')) - | _ -> Constr.map aux t - in - let c' = aux c in - if !changed then c' else 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 (* let substkey = Profile.declare_profile "subst_instance_constr";; *) (* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) |