Fix bug #4673: regression in setoid_rewrite.

Modulo delta for types should be fully transparent.

1 files changed, 1 insertions, 1 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 0892dc9e6c..3a62358e3e 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -576,7 +576,7 @@ let general_rewrite_unif_flags () =
       Unification.modulo_conv_on_closed_terms = Some ts;
       Unification.use_evars_eagerly_in_conv_on_closed_terms = false;
       Unification.modulo_delta = ts;
-      Unification.modulo_delta_types = ts;
+      Unification.modulo_delta_types = full_transparent_state;
       Unification.modulo_betaiota = true }
   in {
     Unification.core_unify_flags = core_flags;