Rename TranspState into TransparentState.

4 files changed, 9 insertions, 9 deletions

diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 820dd97043..6a80525200 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -18,12 +18,12 @@ open Tacticals.New
 open Globnames
 
 let update_flags ()=
-  let open TranspState in
+  let open TransparentState in
   let f accu coe = match coe.Classops.coe_value with
     | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
     | _ -> accu
   in
-  let flags = List.fold_left f TranspState.full (Classops.coercions ()) in
+  let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in
     red_flags:=
     CClosure.RedFlags.red_add_transparent
       CClosure.betaiotazeta
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index e81335037a..92fa94d6dc 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1487,7 +1487,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 				    Eauto.eauto_with_bases
 				      (true,5)
 				      [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
-                                      [Hints.Hint_db.empty TranspState.empty false]
+                                      [Hints.Hint_db.empty TransparentState.empty false]
 				  )
 			   )
 			)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 84c5b4fbe4..6e5e3f9353 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1359,7 +1359,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 		      Eauto.eauto_with_bases
 			(true,5)
 			[(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
-                        [Hints.Hint_db.empty TranspState.empty false]
+                        [Hints.Hint_db.empty TransparentState.empty false]
 		      ]
 		    )
 		  )
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
   }