Don't map_constr_relevance when not needed in subst_instance_constr

This has noticeable perf impact in category_theory
SkySkimmer · Sep 28, 2023 · 8449507 · 8449507
1 parent 724621d
commit 8449507
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/kernel/vars.ml b/kernel/vars.ml
@@ -436,7 +436,9 @@ let subst_instance_constr subst c =
   else
     let f u = UVars.subst_instance_instance subst u in
     let rec aux t =
-      let t = map_constr_relevance (UVars.subst_instance_relevance subst) t in
+      let t = if CArray.is_empty (fst (UVars.Instance.to_array subst)) then t
+        else map_constr_relevance (UVars.subst_instance_relevance subst) t
+      in
       match kind t with
       | Const (c, u) ->
        if UVars.Instance.is_empty u then t