From 5fb30d6c06d47a8e6c4200cdd0ba9067be7cfe2f Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Mon, 12 Jun 2017 17:44:29 +0200
Subject: use map_constr more efficiently

---
 checker/term.ml | 42 ++++++++++++++++++++++++++++++------------
 1 file changed, 30 insertions(+), 12 deletions(-)

(limited to 'checker/term.ml')

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
-- 
cgit v1.2.3