From 695ca081db78c250db58381027e49f4be701672e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 10 Jun 2020 15:49:33 +0200
Subject: Try to preserve more sharing in nf_evars_and_universes_opt_subst.

---
 engine/univSubst.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine')

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
-- 
cgit v1.2.3