From 8449507c2c434d049b32f303e44d5ba78863c5a8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 27 Sep 2023 15:23:41 +0200 Subject: [PATCH] Don't map_constr_relevance when not needed in subst_instance_constr This has noticeable perf impact in category_theory --- kernel/vars.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kernel/vars.ml b/kernel/vars.ml index ed08953dcc1c0..1bd44cdab4fb4 100644 --- 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