Restoring non-uniform delta on local and global constants in 2nd order

unification for apply (compatibility reason). Waiting for another way
to provide a more uniform scheme by default (keyed unification?).

1 files changed, 1 insertions, 1 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f99ea9a52c..a347149e37 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -307,7 +307,7 @@ let default_unify_flags () =
   let flags = default_core_unify_flags () in {
   core_unify_flags = flags;
   merge_unify_flags = flags;
-  subterm_unify_flags = { flags with modulo_delta = empty_transparent_state };
+  subterm_unify_flags = { flags with modulo_delta = var_full_transparent_state };
   allow_K_in_toplevel_higher_order_unification = false; (* Why not? *)
   resolve_evars = false
 }