Try to preserve more sharing in nf_evars_and_universes_opt_subst.

1 files changed, 3 insertions, 3 deletions

diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index a691239ee2..92211d5f3d 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -131,9 +131,9 @@ let nf_evars_and_universes_opt_subst f subst =
   let rec aux c =
     match kind c with
     | Evar (evk, args) ->
-      let args = List.map aux args in
-      (match try f (evk, args) with Not_found -> None with
-      | None -> mkEvar (evk, args)
+      let args' = List.Smart.map aux args in
+      (match try f (evk, args') with Not_found -> None with
+      | None -> if args == args' then c else mkEvar (evk, args')
       | Some c -> aux c)
     | Const pu ->
       let pu' = subst_univs_fn_puniverses lsubst pu in