Use a smart map_constr

2 files changed, 24 insertions, 64 deletions

diff --git a/checker/term.ml b/checker/term.ml
index f604ac4bd..c0f8e0106 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -413,38 +413,18 @@ 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 =
-  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 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; 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 (changed := true; 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 (changed := true; Construct (c, u'))
-      | Sort (Type u) -> 
-         let u' = Univ.subst_instance_universe subst u in
-	   if u' == u then t else 
-	     (changed := true; Sort (sort_of_univ u'))
-      | _ -> map_constr 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 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
 
 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 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;; *)