From 96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 22 Jun 2018 00:43:01 +0200
Subject: Move transparent_state to its own module.

---
 plugins/ltac/rewrite.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 7d917c58fe..1f31a617be 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -537,8 +537,8 @@ let rewrite_core_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
   Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
   Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
-  Unification.modulo_delta = empty_transparent_state;
-  Unification.modulo_delta_types = full_transparent_state;
+  Unification.modulo_delta = TranspState.empty;
+  Unification.modulo_delta_types = TranspState.full;
   Unification.check_applied_meta_types = true;
   Unification.use_pattern_unification = true;
   Unification.use_meta_bound_pattern_unification = true;
@@ -585,12 +585,12 @@ let general_rewrite_unif_flags () =
       Unification.modulo_conv_on_closed_terms = Some ts;
       Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
       Unification.modulo_delta = ts;
-      Unification.modulo_delta_types = full_transparent_state;
+      Unification.modulo_delta_types = TranspState.full;
       Unification.modulo_betaiota = true }
   in {
     Unification.core_unify_flags = core_flags;
     Unification.merge_unify_flags = core_flags;
-    Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = empty_transparent_state };
+    Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = TranspState.empty };
     Unification.allow_K_in_toplevel_higher_order_unification = true;
     Unification.resolve_evars = true
   }
-- 
cgit v1.2.3


From ad5aea737ecc639c31dda84322b3550a4d380b47 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 22 Jun 2018 21:06:01 +0200
Subject: Proper record type and accessors for transparent states.

This is documented in dev/doc/changes.md.
---
 plugins/ltac/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1f31a617be..d66184227e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -528,7 +528,7 @@ let decompose_applied_relation env sigma (c,l) =
 
 let rewrite_db = "rewrite"
 
-let conv_transparent_state = (Id.Pred.empty, Cpred.full)
+let conv_transparent_state = TranspState.cst_full
 
 let rewrite_transparent_state () =
   Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db)
-- 
cgit v1.2.3


From 733cb74a2038ff92156b7209713fc2ea741ccca6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 19 Nov 2018 08:12:28 +0100
Subject: Rename TranspState into TransparentState.

---
 plugins/ltac/rewrite.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index d66184227e..4142fb2412 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -528,7 +528,7 @@ let decompose_applied_relation env sigma (c,l) =
 
 let rewrite_db = "rewrite"
 
-let conv_transparent_state = TranspState.cst_full
+let conv_transparent_state = TransparentState.cst_full
 
 let rewrite_transparent_state () =
   Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db)
@@ -537,8 +537,8 @@ let rewrite_core_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
   Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
   Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
-  Unification.modulo_delta = TranspState.empty;
-  Unification.modulo_delta_types = TranspState.full;
+  Unification.modulo_delta = TransparentState.empty;
+  Unification.modulo_delta_types = TransparentState.full;
   Unification.check_applied_meta_types = true;
   Unification.use_pattern_unification = true;
   Unification.use_meta_bound_pattern_unification = true;
@@ -585,12 +585,12 @@ let general_rewrite_unif_flags () =
       Unification.modulo_conv_on_closed_terms = Some ts;
       Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
       Unification.modulo_delta = ts;
-      Unification.modulo_delta_types = TranspState.full;
+      Unification.modulo_delta_types = TransparentState.full;
       Unification.modulo_betaiota = true }
   in {
     Unification.core_unify_flags = core_flags;
     Unification.merge_unify_flags = core_flags;
-    Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = TranspState.empty };
+    Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = TransparentState.empty };
     Unification.allow_K_in_toplevel_higher_order_unification = true;
     Unification.resolve_evars = true
   }
-- 
cgit v1.2.3