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