diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/univSubst.ml | 6 |
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 |