use map_constr more efficiently

1 files changed, 30 insertions, 12 deletions

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;; *)