Rename TranspState into TransparentState.

44 files changed, 164 insertions, 164 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9c5785758d..30a2967259 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -19,7 +19,7 @@ Names
   Constant.make3 has been removed, use Constant.make2
   Constant.repr3 has been removed, use Constant.repr2
 
-- `Names.transparent_state` has been moved to its own module `TranspState`.
+- `Names.transparent_state` has been moved to its own module `TransparentState`.
   This module gathers utility functions that used to be defined in several
   places.
 
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 5876b7c5c6..eaa12ff702 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -101,7 +101,7 @@ val ppdelta : Mod_subst.delta_resolver -> unit
 
 val pp_idpred : Names.Id.Pred.t -> unit
 val pp_cpred : Names.Cpred.t -> unit
-val pp_transparent_state : TranspState.t -> unit
+val pp_transparent_state : TransparentState.t -> unit
 
 val pp_stack_t : Constr.t Reductionops.Stack.t -> unit
 val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 625a9a7277..7e73609996 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -72,8 +72,8 @@ let with_stats c =
   end else
     Lazy.force c
 
-let all_opaque = TranspState.empty
-let all_transparent = TranspState.full
+let all_opaque = TransparentState.empty
+let all_transparent = TransparentState.full
 
 module type RedFlagsSig = sig
   type reds
@@ -90,8 +90,8 @@ module type RedFlagsSig = sig
   val no_red : reds
   val red_add : reds -> red_kind -> reds
   val red_sub : reds -> red_kind -> reds
-  val red_add_transparent : reds -> TranspState.t -> reds
-  val red_transparent : reds -> TranspState.t
+  val red_add_transparent : reds -> TransparentState.t -> reds
+  val red_transparent : reds -> TransparentState.t
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
   val red_projection : reds -> Projection.t -> bool
@@ -103,13 +103,13 @@ module RedFlags = (struct
   (* [r_const=(false,cl)] means only those in [cl] *)
   (* [r_delta=true] just mean [r_const=(true,[])] *)
 
-  open TranspState
+  open TransparentState
 
   type reds = {
     r_beta : bool;
     r_delta : bool;
     r_eta : bool;
-    r_const : TranspState.t;
+    r_const : TransparentState.t;
     r_zeta : bool;
     r_match : bool;
     r_fix : bool;
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 26710a64d0..b6c87b3732 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -52,10 +52,10 @@ module type RedFlagsSig = sig
   val red_sub : reds -> red_kind -> reds
 
   (** Adds a reduction kind to a set *)
-  val red_add_transparent : reds -> TranspState.t -> reds
+  val red_add_transparent : reds -> TransparentState.t -> reds
 
   (** Retrieve the transparent state of the reduction flags *)
-  val red_transparent : reds -> TranspState.t
+  val red_transparent : reds -> TransparentState.t
 
   (** Build a reduction set from scratch = iter [red_add] on [no_red] *)
   val mkflags : red_kind list -> reds
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index c66beb49b8..fe82353b70 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -82,7 +82,7 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu =
   Cmap.fold fcst cst_opacity accu
 
 let get_transp_state { var_trstate; cst_trstate; _ } =
-  { TranspState.tr_var = var_trstate; tr_cst = cst_trstate }
+  { TransparentState.tr_var = var_trstate; tr_cst = cst_trstate }
 
 let dep_order l2r k1 k2 = match k1, k2 with
 | RelKey _, RelKey _ -> l2r
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 3b51515352..bc06cc21b6 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -41,5 +41,5 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle
 (** Fold over the non-transparent levels of the oracle. Order unspecified. *)
 val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a
 
-val get_transp_state : oracle -> TranspState.t
+val get_transp_state : oracle -> TransparentState.t
 
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index e716972ebe..54c239349d 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,5 +1,5 @@
 Names
-TranspState
+TransparentState
 Uint31
 Univ
 UGraph
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a45a5b3247..fbb481424f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -177,7 +177,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
 
 (* functions of this type can be called from outside the kernel *)
 type 'a extended_conversion_function =
-  ?l2r:bool -> ?reds:TranspState.t -> env ->
+  ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:((existential->constr option) * UGraph.t) ->
   'a -> 'a -> unit
 
@@ -758,7 +758,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
 	()
 
 (* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=TranspState.full) env ?(evars=(fun _->None), universes env) =
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) =
   let evars, univs = evars in
   if Flags.profile then
     let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
@@ -792,11 +792,11 @@ let infer_conv_universes =
       CProfile.profile8 infer_conv_universes_key infer_conv_universes
   else infer_conv_universes
 
-let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full)
+let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
     env univs t1 t2 = 
   infer_conv_universes CONV l2r evars ts env univs t1 t2
 
-let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full)
+let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
     env univs t1 t2 = 
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 9b26e7b3dc..0408dbf057 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -31,7 +31,7 @@ exception NotConvertibleVect of int
 
 type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
 type 'a extended_conversion_function = 
-  ?l2r:bool -> ?reds:TranspState.t -> env ->
+  ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:((existential->constr option) * UGraph.t) ->
   'a -> 'a -> unit
 
@@ -77,15 +77,15 @@ val conv_leq : types extended_conversion_function
 (** These conversion functions are used by module subtyping, which needs to infer
     universe constraints inside the kernel *)
 val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> 
-  ?ts:TranspState.t -> constr infer_conversion_function
+  ?ts:TransparentState.t -> constr infer_conversion_function
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
-  ?ts:TranspState.t -> types infer_conversion_function
+  ?ts:TransparentState.t -> types infer_conversion_function
 
 (** Depending on the universe state functions, this might raise
   [UniverseInconsistency] in addition to [NotConvertible] (for better error
   messages). *)
 val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
-  TranspState.t -> (constr,'a) generic_conversion_function
+  TransparentState.t -> (constr,'a) generic_conversion_function
 
 val default_conv     : conv_pb -> ?l2r:bool -> types kernel_conversion_function
 val default_conv_leq : ?l2r:bool -> types kernel_conversion_function
diff --git a/kernel/transpState.ml b/kernel/transparentState.ml
index 9661dace6a..9661dace6a 100644
--- a/kernel/transpState.ml
+++ b/kernel/transparentState.ml
diff --git a/kernel/transpState.mli b/kernel/transparentState.mli
index f2999c6869..f2999c6869 100644
--- a/kernel/transpState.mli
+++ b/kernel/transparentState.mli
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 46e52121c7..246c90c09d 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -191,7 +191,7 @@ let warn_bytecode_compiler_failed =
 let vm_conv_gen cv_pb env univs t1 t2 =
   if not (typing_flags env).Declarations.enable_VM then
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TranspState.full env univs t1 t2
+      TransparentState.full env univs t1 t2
   else
   try
     let v1 = val_of_constr env t1 in
@@ -200,7 +200,7 @@ let vm_conv_gen cv_pb env univs t1 t2 =
   with Not_found | Invalid_argument _ ->
     warn_bytecode_compiler_failed ();
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TranspState.full env univs t1 t2
+      TransparentState.full env univs t1 t2
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in
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
   }
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 647ef5092f..e02fb33276 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1698,7 +1698,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context !!env) in
         let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in
-        begin match solve_simple_eqn (evar_conv_x TranspState.full) !!env sigma (None,ev,substl inst ev') with
+        begin match solve_simple_eqn (evar_conv_x TransparentState.full) !!env sigma (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
         end;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0c9ad5d094..f370ad7ae2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -29,7 +29,7 @@ open Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-type unify_fun = TranspState.t ->
+type unify_fun = TransparentState.t ->
   env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
 
 let debug_unification = ref (false)
@@ -73,14 +73,14 @@ let coq_unit_judge =
 
 let unfold_projection env evd ts p c =
   let cst = Projection.constant p in
-    if TranspState.is_transparent_constant ts cst then
+    if TransparentState.is_transparent_constant ts cst then
       Some (mkProj (Projection.unfold p, c))
     else None
       
 let eval_flexible_term ts env evd c =
   match EConstr.kind evd c with
   | Const (c, u) ->
-      if TranspState.is_transparent_constant ts c
+      if TransparentState.is_transparent_constant ts c
       then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u))
       else None
   | Rel n ->
@@ -90,7 +90,7 @@ let eval_flexible_term ts env evd c =
        with Not_found -> None)
   | Var id ->
       (try
-         if TranspState.is_transparent_variable ts id then
+         if TransparentState.is_transparent_variable ts id then
 	   env |> lookup_named id |> NamedDecl.get_value
 	 else None
        with Not_found -> None)
@@ -1210,7 +1210,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   | [] ->
     let evd = 
       try Evarsolve.check_evar_instance evd evk rhs
-            (evar_conv_x TranspState.full)
+            (evar_conv_x TransparentState.full)
       with IllTypedInstance _ -> raise (TypingFailed evd)
     in
       Evd.define evk rhs evd
@@ -1353,7 +1353,7 @@ let solve_unconstrained_impossible_cases env evd =
       let j, ctx = coq_unit_judge env in
       let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
       let ty = j_type j in
-      let conv_algo = evar_conv_x TranspState.full in
+      let conv_algo = evar_conv_x TransparentState.full in
       let evd' = check_evar_instance evd' evk ty conv_algo in
         Evd.define evk ty evd'
     | _ -> evd') evd evd
@@ -1392,7 +1392,7 @@ let solve_unif_constraints_with_heuristics env
 
 exception UnableToUnify of evar_map * unification_error
 
-let default_transparent_state env = TranspState.full
+let default_transparent_state env = TransparentState.full
 (* Conv_oracle.get_transp_state (Environ.oracle env) *)
 
 let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 721a6fad8e..4585fac252 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -21,20 +21,20 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error
 (** {6 Main unification algorithm for type inference. } *)
 
 (** returns exception NotUnifiable with best known evar_map if not unifiable *)
-val the_conv_x     : env -> ?ts:TranspState.t -> constr -> constr -> evar_map -> evar_map
-val the_conv_x_leq : env -> ?ts:TranspState.t -> constr -> constr -> evar_map -> evar_map
+val the_conv_x     : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
+val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
 
 (** The same function resolving evars by side-effect and
    catching the exception *)
-val conv : env -> ?ts:TranspState.t -> evar_map -> constr -> constr -> evar_map option
-val cumul : env -> ?ts:TranspState.t -> evar_map -> constr -> constr -> evar_map option
+val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
+val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
 
 (** {6 Unification heuristics. } *)
 
 (** Try heuristics to solve pending unification problems and to solve
     evars with candidates *)
 
-val solve_unif_constraints_with_heuristics : env -> ?ts:TranspState.t -> evar_map -> evar_map
+val solve_unif_constraints_with_heuristics : env -> ?ts:TransparentState.t -> evar_map -> evar_map
 
 (** Check all pending unification problems are solved and raise an
     error otherwise *)
@@ -54,14 +54,14 @@ val check_conv_record : env -> evar_map ->
 (** Try to solve problems of the form ?x[args] = c by second-order
     matching, using typing to select occurrences *)
 
-val second_order_matching : TranspState.t -> env -> evar_map ->
+val second_order_matching : TransparentState.t -> env -> evar_map ->
   EConstr.existential -> occurrences option list -> constr -> evar_map * bool
 
 (** Declare function to enforce evars resolution by using typing constraints *)
 
 val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit
 
-type unify_fun = TranspState.t ->
+type unify_fun = TransparentState.t ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
 
 (** Override default [evar_conv_x] algorithm. *)
@@ -72,7 +72,7 @@ val evar_conv_x : unify_fun
 
 (**/**)
 (* For debugging *)
-val evar_eqappr_x : ?rhs_is_already_stuck:bool -> TranspState.t * bool ->
+val evar_eqappr_x : ?rhs_is_already_stuck:bool -> TransparentState.t * bool ->
   env -> evar_map ->
     conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
       Evarsolve.unification_result
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4fbbf20c1f..e632976ae5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1301,13 +1301,13 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red
   with Reduction.NotConvertible -> false
     | e when is_anomaly e -> report_anomaly e
 
-let is_conv ?(reds=TranspState.full) env sigma = test_trans_conversion f_conv reds env sigma
-let is_conv_leq ?(reds=TranspState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma
-let is_fconv ?(reds=TranspState.full) = function
+let is_conv ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv reds env sigma
+let is_conv_leq ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma
+let is_fconv ?(reds=TransparentState.full) = function
   | Reduction.CONV -> is_conv ~reds
   | Reduction.CUMUL -> is_conv_leq ~reds
 
-let check_conv ?(pb=Reduction.CUMUL) ?(ts=TranspState.full) env sigma x y =
+let check_conv ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y =
   let f = match pb with
     | Reduction.CONV -> f_conv
     | Reduction.CUMUL -> f_conv_leq
@@ -1341,7 +1341,7 @@ let sigma_univ_state =
     compare_cumul_instances = sigma_check_inductive_instances; }
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
-    ?(ts=TranspState.full) env sigma x y =
+    ?(ts=TransparentState.full) env sigma x y =
   (** FIXME *)
   try
       let ans = match pb with
@@ -1374,7 +1374,7 @@ let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
       Reduction.generic_conv pb ~l2r (safe_evar_value sigma))
 
 (* This reference avoids always having to link C code with the kernel *)
-let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:TranspState.full)
+let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:TransparentState.full)
 let set_vm_infer_conv f = vm_infer_conv := f
 let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
   !vm_infer_conv ~pb env t1 t2
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 749e23bde2..088e898a99 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -266,21 +266,21 @@ type conversion_test = Constraint.t -> Constraint.t
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
-val is_conv : ?reds:TranspState.t -> env -> evar_map -> constr -> constr -> bool
-val is_conv_leq : ?reds:TranspState.t -> env ->  evar_map -> constr -> constr -> bool
-val is_fconv : ?reds:TranspState.t -> conv_pb -> env ->  evar_map -> constr -> constr -> bool
+val is_conv : ?reds:TransparentState.t -> env -> evar_map -> constr -> constr -> bool
+val is_conv_leq : ?reds:TransparentState.t -> env ->  evar_map -> constr -> constr -> bool
+val is_fconv : ?reds:TransparentState.t -> conv_pb -> env ->  evar_map -> constr -> constr -> bool
 
 (** [check_conv] Checks universe constraints only.
     pb defaults to CUMUL and ts to a full transparent state.
  *)
-val check_conv : ?pb:conv_pb -> ?ts:TranspState.t -> env ->  evar_map -> constr -> constr -> bool
+val check_conv : ?pb:conv_pb -> ?ts:TransparentState.t -> env ->  evar_map -> constr -> constr -> bool
 
 (** [infer_conv] Adds necessary universe constraints to the evar map.
     pb defaults to CUMUL and ts to a full transparent state.
     @raise UniverseInconsistency iff catch_incon is set to false,
     otherwise returns false in that case.
  *)
-val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TranspState.t ->
+val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t ->
   env -> evar_map -> constr -> constr -> evar_map option
 
 (** Conversion with inference of universe constraints *)
@@ -292,9 +292,9 @@ val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
 
 (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
 conversion function. Used to pretype vm and native casts. *)
-val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TranspState.t ->
+val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t ->
     (Constr.constr, evar_map) Reduction.generic_conversion_function) ->
-  ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TranspState.t -> env ->
+  ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env ->
   evar_map -> constr -> constr -> evar_map option
 
 (** {6 Special-Purpose Reduction Functions } *)
@@ -307,7 +307,7 @@ val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
 (** {6 Heuristic for Conversion with Evar } *)
 
 val whd_betaiota_deltazeta_for_iota_state :
-  TranspState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state ->
+  TransparentState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state ->
   state * Cst_stack.t
 
 (** {6 Meta-related reduction functions } *)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c6a58fc1e9..8bdac0a575 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -119,8 +119,8 @@ val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types ->
 val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t
 val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
 
-val classes_transparent_state_hook : (unit -> TranspState.t) Hook.t
-val classes_transparent_state : unit -> TranspState.t
+val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t
+val classes_transparent_state : unit -> TransparentState.t
 
 val add_instance_hint_hook :
   (global_reference_or_constr -> GlobRef.t list ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 99b8d8e92a..490d58fa52 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -149,7 +149,7 @@ let abstract_list_all_with_dependencies env evd typ c l =
   let n = List.length l in
   let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
   let evd,b =
-    Evarconv.second_order_matching TranspState.empty
+    Evarconv.second_order_matching TransparentState.empty
       env evd ev' argoccs c in
   if b then
     let p = nf_evar evd ev in
@@ -247,7 +247,7 @@ let sort_eqns = unify_r2l
 *)
 
 type core_unify_flags = {
-  modulo_conv_on_closed_terms : TranspState.t option;
+  modulo_conv_on_closed_terms : TransparentState.t option;
     (* What this flag controls was activated with all constants transparent, *)
     (* even for auto, since Coq V5.10 *)
 
@@ -257,11 +257,11 @@ type core_unify_flags = {
 
   use_evars_eagerly_in_conv_on_closed_terms : bool;
 
-  modulo_delta : TranspState.t;
+  modulo_delta : TransparentState.t;
     (* This controls which constants are unfoldable; this is on for apply *)
     (* (but not simple apply) since Feb 2008 for 8.2 *)
 
-  modulo_delta_types : TranspState.t;
+  modulo_delta_types : TransparentState.t;
 
   check_applied_meta_types : bool;
     (* This controls whether meta's applied to arguments have their *)
@@ -322,7 +322,7 @@ type unify_flags = {
 (* Default flag for unifying a type against a type (e.g. apply) *)
 (* We set all conversion flags (no flag should be modified anymore) *)
 let default_core_unify_flags () =
-  let ts = TranspState.full in {
+  let ts = TransparentState.full in {
   modulo_conv_on_closed_terms = Some ts;
   use_metas_eagerly_in_conv_on_closed_terms = true;
   use_evars_eagerly_in_conv_on_closed_terms = false;
@@ -344,14 +344,14 @@ 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 = TranspState.var_full };
+  subterm_unify_flags = { flags with modulo_delta = TransparentState.var_full };
   allow_K_in_toplevel_higher_order_unification = false; (* Why not? *)
   resolve_evars = false
 }
 
 let set_no_delta_core_flags flags = { flags with
   modulo_conv_on_closed_terms = None;
-  modulo_delta = TranspState.empty;
+  modulo_delta = TransparentState.empty;
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true;
@@ -370,7 +370,7 @@ let set_no_delta_flags flags = {
 (* For the first phase of keyed unification, restrict
   to conversion (including beta-iota) only on closed terms *)
 let set_no_delta_open_core_flags flags = { flags with
-  modulo_delta = TranspState.empty;
+  modulo_delta = TransparentState.empty;
   modulo_betaiota = false;
 }
 
@@ -388,7 +388,7 @@ let set_no_delta_open_flags flags = {
 (* We set only the flags available at the time the new "apply" extended *)
 (* out of "simple apply" *)
 let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with
-  modulo_delta = TranspState.empty;
+  modulo_delta = TransparentState.empty;
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true;
@@ -425,7 +425,7 @@ let elim_flags_evars sigma =
   let flags = elim_core_flags sigma in {
   core_unify_flags = flags;
   merge_unify_flags = flags;
-  subterm_unify_flags = { flags with modulo_delta = TranspState.empty };
+  subterm_unify_flags = { flags with modulo_delta = TransparentState.empty };
   allow_K_in_toplevel_higher_order_unification = true;
   resolve_evars = false
 }
@@ -433,7 +433,7 @@ let elim_flags_evars sigma =
 let elim_flags () = elim_flags_evars Evd.empty
 
 let elim_no_delta_core_flags () = { (elim_core_flags Evd.empty) with
-  modulo_delta = TranspState.empty;
+  modulo_delta = TransparentState.empty;
   check_applied_meta_types = false;
   use_pattern_unification = false;
   modulo_betaiota = false;
@@ -504,16 +504,16 @@ let key_of env sigma b flags f =
   if subterm_restriction b flags then None else
   match EConstr.kind sigma f with
   | Const (cst, u) when is_transparent env (ConstKey cst) &&
-      (TranspState.is_transparent_constant flags.modulo_delta cst
+      (TransparentState.is_transparent_constant flags.modulo_delta cst
        || Recordops.is_primitive_projection cst) ->
       let u = EInstance.kind sigma u in
       Some (IsKey (ConstKey (cst, u)))
   | Var id when is_transparent env (VarKey id) && 
-      TranspState.is_transparent_variable flags.modulo_delta id ->
+      TransparentState.is_transparent_variable flags.modulo_delta id ->
     Some (IsKey (VarKey id))
   | Proj (p, c) when Projection.unfolded p
     || (is_transparent env (ConstKey (Projection.constant p)) &&
-       (TranspState.is_transparent_constant flags.modulo_delta (Projection.constant p))) ->
+       (TransparentState.is_transparent_constant flags.modulo_delta (Projection.constant p))) ->
     Some (IsProj (p, c))
   | _ -> None
   
@@ -550,7 +550,7 @@ let oracle_order env cf1 cf2 =
 
 let is_rigid_head sigma flags t =
   match EConstr.kind sigma t with
-  | Const (cst,u) -> not (TranspState.is_transparent_constant flags.modulo_delta cst)
+  | Const (cst,u) -> not (TransparentState.is_transparent_constant flags.modulo_delta cst)
   | Ind (i,u) -> true
   | Construct _ -> true
   | Fix _ | CoFix _ -> true
@@ -633,11 +633,11 @@ let rec is_neutral env sigma ts t =
     | Const (c, u) ->
       not (Environ.evaluable_constant c env) ||
       not (is_transparent env (ConstKey c)) ||
-      not (TranspState.is_transparent_constant ts c)
+      not (TransparentState.is_transparent_constant ts c)
     | Var id -> 
       not (Environ.evaluable_named id env) ||
       not (is_transparent env (VarKey id)) ||
-      not (TranspState.is_transparent_variable ts id)
+      not (TransparentState.is_transparent_variable ts id)
     | Rel n -> true
     | Evar _ | Meta _ -> true
     | Case (_, p, c, cl) -> is_neutral env sigma ts c
@@ -935,8 +935,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	let ty1 = get_type_of curenv ~lax:true sigma c1 in
 	let ty2 = get_type_of curenv ~lax:true sigma c2 in
 	  unify_0_with_initial_metas substn true curenv cv_pb
-            { flags with modulo_conv_on_closed_terms = Some TranspState.full;
-              modulo_delta = TranspState.full;
+            { flags with modulo_conv_on_closed_terms = Some TransparentState.full;
+              modulo_delta = TransparentState.full;
 	      modulo_eta = true;
 	      modulo_betaiota = true }
 	    ty1 ty2
@@ -1121,9 +1121,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       | None ->
         if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
         | Some cv, dl ->
-          let open TranspState in
+          let open TransparentState in
           Id.Pred.subset dl.tr_var cv.tr_var && Cpred.subset dl.tr_cst cv.tr_cst
-        | None, dl -> TranspState.is_empty dl)
+        | None, dl -> TransparentState.is_empty dl)
 	then error_cannot_unify env sigma (m, n) else None
   in 
     let a = match res with 
@@ -1263,8 +1263,8 @@ let applyHead env evd n c  =
 
 let is_mimick_head sigma ts f =
   match EConstr.kind sigma f with
-  | Const (c,u) -> not (TranspState.is_transparent_constant ts c)
-  | Var id -> not (TranspState.is_transparent_variable ts id)
+  | Const (c,u) -> not (TransparentState.is_transparent_constant ts c)
+  | Var id -> not (TransparentState.is_transparent_variable ts id)
   | (Rel _|Construct _|Ind _) -> true
   | _ -> false
 
@@ -1534,11 +1534,11 @@ let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sig
   (sigma, nf_evar sigma c)
 
 let default_matching_core_flags sigma =
-  let ts = TranspState.full in {
-  modulo_conv_on_closed_terms = Some TranspState.empty;
+  let ts = TransparentState.full in {
+  modulo_conv_on_closed_terms = Some TransparentState.empty;
   use_metas_eagerly_in_conv_on_closed_terms = false;
   use_evars_eagerly_in_conv_on_closed_terms = false;
-  modulo_delta = TranspState.empty;
+  modulo_delta = TransparentState.empty;
   modulo_delta_types = ts;
   check_applied_meta_types = true;
   use_pattern_unification = false;
@@ -1550,7 +1550,7 @@ let default_matching_core_flags sigma =
 }
 
 let default_matching_merge_flags sigma =
-  let ts = TranspState.full in
+  let ts = TransparentState.full in
   let flags = default_matching_core_flags sigma in {
   flags with
     modulo_conv_on_closed_terms = Some ts;
@@ -1580,7 +1580,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
     if from_prefix_of_ind then
       let flags = default_matching_flags pending in
       { flags with core_unify_flags = { flags.core_unify_flags with
-        modulo_conv_on_closed_terms = Some TranspState.full;
+        modulo_conv_on_closed_terms = Some TransparentState.full;
         restrict_conv_on_strict_subterms = true } }
     else default_matching_flags pending in
   let n = Array.length (snd (decompose_app_vect sigma c)) in
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index b7b525c9fc..a45b8f1dd8 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -14,11 +14,11 @@ open Environ
 open Evd
 
 type core_unify_flags = {
-  modulo_conv_on_closed_terms : TranspState.t option;
+  modulo_conv_on_closed_terms : TransparentState.t option;
   use_metas_eagerly_in_conv_on_closed_terms : bool;
   use_evars_eagerly_in_conv_on_closed_terms : bool;
-  modulo_delta : TranspState.t;
-  modulo_delta_types : TranspState.t;
+  modulo_delta : TransparentState.t;
+  modulo_delta_types : TransparentState.t;
   check_applied_meta_types : bool;
   use_pattern_unification : bool;
   use_meta_bound_pattern_unification : bool;
@@ -40,7 +40,7 @@ val default_core_unify_flags : unit -> core_unify_flags
 val default_no_delta_core_unify_flags : unit -> core_unify_flags
 
 val default_unify_flags : unit -> unify_flags
-val default_no_delta_unify_flags : TranspState.t -> unify_flags
+val default_no_delta_unify_flags : TransparentState.t -> unify_flags
 
 val elim_flags : unit -> unify_flags
 val elim_no_delta_flags : unit -> unify_flags
diff --git a/printing/printer.ml b/printing/printer.ml
index b7c53c5513..dfe987a671 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -446,8 +446,8 @@ let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
 let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p)
 
 let pr_transparent_state ts =
-  hv 0 (str"VARIABLES: " ++ pr_idpred ts.TranspState.tr_var ++ fnl () ++
-        str"CONSTANTS: " ++ pr_cpred ts.TranspState.tr_cst ++ fnl ())
+  hv 0 (str"VARIABLES: " ++ pr_idpred ts.TransparentState.tr_var ++ fnl () ++
+        str"CONSTANTS: " ++ pr_cpred ts.TransparentState.tr_cst ++ fnl ())
 
 (* display complete goal
  og_s has goal+sigma on the previous proof step for diffs
diff --git a/printing/printer.mli b/printing/printer.mli
index fb4e790c10..cfa1caef00 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -134,7 +134,7 @@ val pr_context_of          : env -> evar_map -> Pp.t
 val pr_predicate           : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t
 val pr_cpred               : Cpred.t -> Pp.t
 val pr_idpred              : Id.Pred.t -> Pp.t
-val pr_transparent_state   : TranspState.t -> Pp.t
+val pr_transparent_state   : TransparentState.t -> Pp.t
 
 (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ac3f52c6ef..c7703b52c7 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -101,11 +101,11 @@ let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv =
    provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
 
 let fail_quick_core_unif_flags = {
-  modulo_conv_on_closed_terms = Some TranspState.full;
+  modulo_conv_on_closed_terms = Some TransparentState.full;
   use_metas_eagerly_in_conv_on_closed_terms = false;
   use_evars_eagerly_in_conv_on_closed_terms = false;
-  modulo_delta = TranspState.empty;
-  modulo_delta_types = TranspState.full;
+  modulo_delta = TransparentState.empty;
+  modulo_delta_types = TransparentState.full;
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true; (* ? *)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index fb42a9cebe..6c4193c66b 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -37,7 +37,7 @@ let define_and_solve_constraints evk c env evd =
   match
     List.fold_left
       (fun p (pbty,env,t1,t2) -> match p with
-        | Success evd -> Evarconv.evar_conv_x TranspState.full env evd pbty t1 t2
+        | Success evd -> Evarconv.evar_conv_x TransparentState.full env evd pbty t1 t2
 	| UnifFailure _ as x -> x) (Success evd)
       pbs
   with
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 1aaf762e31..0981584bb5 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -160,7 +160,7 @@ let make_flag env f =
 	  (fun v red -> red_sub red (make_flag_constant v))
 	  f.rConst red
     else (* Only rConst *)
-        let red = red_add_transparent (red_add red fDELTA) TranspState.empty in
+        let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in
 	List.fold_right
 	  (fun v red -> red_add red (make_flag_constant v))
 	  f.rConst red
diff --git a/tactics/auto.ml b/tactics/auto.ml
index a23a085db5..81e487b77d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -45,7 +45,7 @@ let auto_core_unif_flags_of st1 st2 = {
   use_metas_eagerly_in_conv_on_closed_terms = false;
   use_evars_eagerly_in_conv_on_closed_terms = false;
   modulo_delta = st2;
-  modulo_delta_types = TranspState.full;
+  modulo_delta_types = TransparentState.full;
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true;
@@ -59,13 +59,13 @@ let auto_unif_flags_of st1 st2 =
   let flags = auto_core_unif_flags_of st1 st2 in {
   core_unify_flags = flags;
   merge_unify_flags = flags;
-  subterm_unify_flags = { flags with modulo_delta = TranspState.empty };
+  subterm_unify_flags = { flags with modulo_delta = TransparentState.empty };
   allow_K_in_toplevel_higher_order_unification = false;
   resolve_evars = true
 }
 
 let auto_unif_flags =
-  auto_unif_flags_of TranspState.full TranspState.empty
+  auto_unif_flags_of TransparentState.full TransparentState.empty
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
@@ -291,7 +291,7 @@ let flags_of_state st =
   auto_unif_flags_of st st
 
 let auto_flags_of_state st =
-  auto_unif_flags_of TranspState.full st
+  auto_unif_flags_of TransparentState.full st
 
 let hintmap_of sigma secvars hdc concl =
   match hdc with
@@ -363,7 +363,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 	    let l =
 	      match hdc with None -> Hint_db.map_none ~secvars db
 	      | Some hdc ->
-                  if TranspState.is_empty st
+                  if TransparentState.is_empty st
 		  then Hint_db.map_auto sigma ~secvars hdc concl db
 		  else Hint_db.map_existential sigma ~secvars hdc concl db
 	    in auto_flags_of_state st, l
diff --git a/tactics/auto.mli b/tactics/auto.mli
index c7acbd4bfb..72d2292ffb 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -22,7 +22,7 @@ val compute_secvars : Proofview.Goal.t -> Id.Pred.t
 
 val default_search_depth : int ref
 
-val auto_flags_of_state : TranspState.t -> Unification.unify_flags
+val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
 
 val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
   Proofview.Goal.t -> clausenv * constr
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 04fe6a9fa7..2f2bd8d2bc 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -72,10 +72,10 @@ let constr_pat_discr t =
 let constr_val_discr_st sigma ts t =
   let c, l = decomp sigma t in
     match EConstr.kind sigma c with
-    | Const (c,u) -> if TranspState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l)
+    | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l)
     | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
     | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
-    | Var id when not (TranspState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l)
+    | Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Label(ProdLabel, [d; c])
     | Lambda (n, d, c) -> 
       if List.is_empty l then 
@@ -89,11 +89,11 @@ let constr_pat_discr_st ts t =
   match decomp_pat t with
   | PRef ((IndRef _) as ref), args
   | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
-  | PRef ((VarRef v) as ref), args when not (TranspState.is_transparent_variable ts v) ->
+  | PRef ((VarRef v) as ref), args when not (TransparentState.is_transparent_variable ts v) ->
       Some(GRLabel ref,args)
-  | PVar v, args when not (TranspState.is_transparent_variable ts v) ->
+  | PVar v, args when not (TransparentState.is_transparent_variable ts v) ->
       Some(GRLabel (VarRef v),args)
-  | PRef ((ConstRef c) as ref), args when not (TranspState.is_transparent_constant ts c) ->
+  | PRef ((ConstRef c) as ref), args when not (TransparentState.is_transparent_constant ts c) ->
       Some (GRLabel ref, args)
   | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
   | PLambda (_, d, c), [] -> Some (LambdaLabel, [d ; c])
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 6af5012def..cc31fb0599 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -18,7 +18,7 @@ open Pattern
 order in such a way patterns having the same prefix have this common
 prefix shared and the seek for the action associated to the patterns
 that a term matches are found in time proportional to the maximal
-number of nodes of the patterns matching the term. The [TranspState.t]
+number of nodes of the patterns matching the term. The [TransparentState.t]
 indicates which constants and variables can be considered as rigid.
 These dnets are able to cope with existential variables as well, which match
 [Everything]. *)
@@ -30,10 +30,10 @@ sig
 
   val empty : t
 
-  val add : TranspState.t option -> t -> (constr_pattern * Z.t) -> t
-  val rmv : TranspState.t option -> t -> (constr_pattern * Z.t) -> t
+  val add : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t
+  val rmv : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t
 
-  val lookup : Evd.evar_map -> TranspState.t option -> t -> EConstr.constr -> Z.t list
+  val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list
   val app : (Z.t -> unit) -> t -> unit
 end
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f27e5e281a..1bb33f2a23 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -585,9 +585,9 @@ module Search = struct
   (** Local hints *)
   let autogoal_cache = Summary.ref ~name:"autogoal_cache"
       (DirPath.empty, true, Context.Named.empty,
-       Hint_db.empty TranspState.full true)
+       Hint_db.empty TransparentState.full true)
 
-  let make_autogoal_hints only_classes ?(st=TranspState.full) g =
+  let make_autogoal_hints only_classes ?(st=TransparentState.full) g =
     let open Proofview in
     let open Tacmach.New in
     let sign = Goal.hyps g in
@@ -605,7 +605,7 @@ module Search = struct
       in
       autogoal_cache := (cwd, only_classes, sign, hints); hints
 
-  let make_autogoal ?(st=TranspState.full) only_classes dep cut i g =
+  let make_autogoal ?(st=TransparentState.full) only_classes dep cut i g =
     let hints = make_autogoal_hints only_classes ~st g in
     { search_hints = hints;
       search_depth = [i]; last_tac = lazy (str"none");
@@ -843,7 +843,7 @@ module Search = struct
     let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
     search_tac hints depth 1 info
 
-  let search_tac ?(st=TranspState.full) only_classes dep hints depth =
+  let search_tac ?(st=TransparentState.full) only_classes dep hints depth =
     let open Proofview in
     let tac sigma gls i =
       Goal.enter
@@ -873,7 +873,7 @@ module Search = struct
                                    | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
-  let eauto_tac ?(st=TranspState.full) ?(unique=false)
+  let eauto_tac ?(st=TransparentState.full) ?(unique=false)
                 ~only_classes ?strategy ~depth ~dep hints =
     let open Proofview in
     let tac =
@@ -985,7 +985,7 @@ end
 
 (** Binding to either V85 or Search implementations. *)
 
-let typeclasses_eauto ?(only_classes=false) ?(st=TranspState.full)
+let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
                       ?strategy ~depth dbs =
   let dbs = List.map_filter
               (fun db -> try Some (searchtable_map db)
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 9e2b0d26b5..46dff34f89 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -25,7 +25,7 @@ type search_strategy = Dfs | Bfs
 
 val set_typeclasses_strategy : search_strategy -> unit
 
-val typeclasses_eauto : ?only_classes:bool -> ?st:TranspState.t -> ?strategy:search_strategy ->
+val typeclasses_eauto : ?only_classes:bool -> ?st:TransparentState.t -> ?strategy:search_strategy ->
                         depth:(Int.t option) ->
                         Hints.hint_db_name list -> unit Proofview.tactic
 
@@ -39,7 +39,7 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
 
 module Search : sig
   val eauto_tac :
-    ?st:TranspState.t ->
+    ?st:TransparentState.t ->
     (** The transparent_state used when working with local hypotheses  *)
     ?unique:bool ->
     (** Should we force a unique solution *)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index c18b7bb214..9a6bdab7b9 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -29,7 +29,7 @@ open Locusops
 open Hints
 open Proofview.Notations
 
-let eauto_unif_flags = auto_flags_of_state TranspState.full
+let eauto_unif_flags = auto_flags_of_state TransparentState.full
 
 let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter begin fun gl ->
@@ -307,7 +307,7 @@ module SearchProblem = struct
 		     let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in
 		     let hyps' = pf_hyps gls in
 		       if hyps' == hyps then List.hd s.localdb
-                       else make_local_hint_db (pf_env gls) (project gls) ~ts:TranspState.full true s.local_lemmas)
+                       else make_local_hint_db (pf_env gls) (project gls) ~ts:TransparentState.full true s.local_lemmas)
 		     (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
 	       in
 		 { depth = pred s.depth; priority = cost; tacres = lgls;
@@ -388,7 +388,7 @@ let make_initial_state dbg n gl dblist localdb lems =
   }
 
 let e_search_auto debug (in_depth,p) lems db_list gl =
-  let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:TranspState.full true lems in
+  let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:TransparentState.full true lems in
   let d = mk_eauto_dbg debug in
   let tac = match in_depth,d with
     | (true,Debug) -> Search.debug_depth_first
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8377cd5c75..969f539d1f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -101,8 +101,8 @@ let rewrite_core_unif_flags = {
   modulo_conv_on_closed_terms = None;
   use_metas_eagerly_in_conv_on_closed_terms = true;
   use_evars_eagerly_in_conv_on_closed_terms = false;
-  modulo_delta = TranspState.empty;
-  modulo_delta_types = TranspState.empty;
+  modulo_delta = TransparentState.empty;
+  modulo_delta_types = TransparentState.empty;
   check_applied_meta_types = true;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
@@ -169,7 +169,7 @@ let instantiate_lemma gl c ty l l2r concl =
   [eqclause]
 
 let rewrite_conv_closed_core_unif_flags = {
-  modulo_conv_on_closed_terms = Some TranspState.full;
+  modulo_conv_on_closed_terms = Some TransparentState.full;
     (* We have this flag for historical reasons, it has e.g. the consequence *)
     (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *)
 
@@ -178,8 +178,8 @@ let rewrite_conv_closed_core_unif_flags = {
     (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *)
     (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *)
 
-  modulo_delta = TranspState.empty;
-  modulo_delta_types = TranspState.full;
+  modulo_delta = TransparentState.empty;
+  modulo_delta_types = TransparentState.full;
   check_applied_meta_types = true;
   use_pattern_unification = true;
     (* To rewrite "?n x y" in "y+x=0" when ?n is *)
@@ -204,7 +204,7 @@ let rewrite_conv_closed_unif_flags = {
 }
 
 let rewrite_keyed_core_unif_flags = {
-  modulo_conv_on_closed_terms = Some TranspState.full;
+  modulo_conv_on_closed_terms = Some TransparentState.full;
     (* We have this flag for historical reasons, it has e.g. the consequence *)
     (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *)
 
@@ -213,8 +213,8 @@ let rewrite_keyed_core_unif_flags = {
     (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *)
     (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *)
 
-  modulo_delta = TranspState.full;
-  modulo_delta_types = TranspState.full;
+  modulo_delta = TransparentState.full;
+  modulo_delta_types = TransparentState.full;
   check_applied_meta_types = true;
   use_pattern_unification = true;
     (* To rewrite "?n x y" in "y+x=0" when ?n is *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 287e289c2f..6aa021543d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -291,8 +291,8 @@ let lookup_tacs sigma concl st se =
 module Constr_map = Map.Make(GlobRef.Ordered)
 
 let is_transparent_gr ts = function
-  | VarRef id -> TranspState.is_transparent_variable ts id
-  | ConstRef cst -> TranspState.is_transparent_constant ts cst
+  | VarRef id -> TransparentState.is_transparent_variable ts id
+  | ConstRef cst -> TransparentState.is_transparent_constant ts cst
   | IndRef _ | ConstructRef _ -> false
 
 let strip_params env sigma c = 
@@ -497,7 +497,7 @@ type hint_db_name = string
 module Hint_db :
 sig
 type t
-val empty : ?name:hint_db_name -> TranspState.t -> bool -> t
+val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
 val find : GlobRef.t -> t -> search_entry
 val map_none : secvars:Id.Pred.t -> t -> full_hint list
 val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
@@ -513,8 +513,8 @@ val remove_one : GlobRef.t -> t -> t
 val remove_list : GlobRef.t list -> t -> t
 val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
 val use_dn : t -> bool
-val transparent_state : t -> TranspState.t
-val set_transparent_state : t -> TranspState.t -> t
+val transparent_state : t -> TransparentState.t
+val set_transparent_state : t -> TransparentState.t -> t
 val add_cut : hints_path -> t -> t
 val add_mode : GlobRef.t -> hint_mode array -> t -> t
 val cut : t -> hints_path
@@ -526,7 +526,7 @@ end =
 struct
 
   type t = {
-    hintdb_state : TranspState.t;
+    hintdb_state : TransparentState.t;
     hintdb_cut : hints_path;
     hintdb_unfolds : Id.Set.t * Cset.t;
     hintdb_max_id : int;
@@ -664,7 +664,7 @@ struct
       match v.code.obj with
       | Unfold_nth egr ->
           let addunf ts (ids, csts) =
-            let open TranspState in
+            let open TransparentState in
 	    match egr with
             | EvalVarRef id ->
               { ts with tr_var = Id.Pred.add id ts.tr_var }, (Id.Set.add id ids, csts)
@@ -743,8 +743,8 @@ let typeclasses_db = "typeclass_instances"
 let rewrite_db = "rewrite"
 
 let auto_init_db =
-  Hintdbmap.add typeclasses_db (Hint_db.empty TranspState.full true)
-    (Hintdbmap.add rewrite_db (Hint_db.empty TranspState.cst_full true)
+  Hintdbmap.add typeclasses_db (Hint_db.empty TransparentState.full true)
+    (Hintdbmap.add rewrite_db (Hint_db.empty TransparentState.cst_full true)
        Hintdbmap.empty)
 
 let searchtable = Summary.ref ~name:"searchtable" auto_init_db
@@ -980,7 +980,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
 
 let get_db dbname =
   try searchtable_map dbname
-  with Not_found -> Hint_db.empty ~name:dbname TranspState.empty false
+  with Not_found -> Hint_db.empty ~name:dbname TransparentState.empty false
 
 let add_hint dbname hintlist =
   let check (_, h) =
@@ -998,7 +998,7 @@ let add_hint dbname hintlist =
     searchtable_add (dbname,db')
 
 let add_transparency dbname target b =
-  let open TranspState in
+  let open TransparentState in
   let db = get_db dbname in
   let st = Hint_db.transparent_state db in
   let st' =
@@ -1019,7 +1019,7 @@ let remove_hint dbname grs =
     searchtable_add (dbname, db')
 
 type hint_action =
-  | CreateDB of bool * TranspState.t
+  | CreateDB of bool * TransparentState.t
   | AddTransparency of evaluable_global_reference hints_transparency_target * bool
   | AddHints of hint_entry list
   | RemoveHints of GlobRef.t list
@@ -1547,7 +1547,7 @@ let pr_hint_db_env env sigma db =
     in
     Hint_db.fold fold db (mt ())
   in
-  let { TranspState.tr_var = ids; tr_cst = csts } = Hint_db.transparent_state db in
+  let { TransparentState.tr_var = ids; tr_cst = csts } = Hint_db.transparent_state db in
   hov 0
     ((if Hint_db.use_dn db then str"Discriminated database"
       else str"Non-discriminated database")) ++ fnl () ++
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 43cfb6a059..dd2c63d351 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -122,7 +122,7 @@ val glob_hints_path :
 module Hint_db :
   sig
     type t
-    val empty : ?name:hint_db_name -> TranspState.t -> bool -> t
+    val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
     val find : GlobRef.t -> t -> search_entry
 
     (** All hints which have no pattern.
@@ -155,8 +155,8 @@ module Hint_db :
                 hint_mode array list -> full_hint list -> unit) -> t -> unit
 
     val use_dn : t -> bool
-    val transparent_state : t -> TranspState.t
-    val set_transparent_state : t -> TranspState.t -> t
+    val transparent_state : t -> TransparentState.t
+    val set_transparent_state : t -> TransparentState.t -> t
 
     val add_cut : hints_path -> t -> t
     val cut : t -> hints_path
@@ -191,7 +191,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit
    [use_dn] switches the use of the discrimination net for all hints
    and patterns. *)
 
-val create_hint_db : bool -> hint_db_name -> TranspState.t -> bool -> unit
+val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit
 
 val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit
 
@@ -273,7 +273,7 @@ val repr_hint : hint -> (raw_hint * clausenv) hint_ast
    Useful to take the current goal hypotheses as hints;
    Boolean tells if lemmas with evars are allowed *)
 
-val make_local_hint_db : env -> evar_map -> ?ts:TranspState.t -> bool -> delayed_open_constr list -> hint_db
+val make_local_hint_db : env -> evar_map -> ?ts:TransparentState.t -> bool -> delayed_open_constr list -> hint_db
 
 val make_db_list : hint_db_name list -> hint_db list
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2601b5fd84..349cfce205 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1660,7 +1660,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
     let sigma = Tacmach.New.project gl in
     let ts =
       if respect_opaque then Conv_oracle.get_transp_state (oracle env)
-      else TranspState.full
+      else TransparentState.full
     in
     let flags =
       if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
@@ -1826,7 +1826,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
     let sigma = Tacmach.New.project gl in
     let ts =
       if respect_opaque then Conv_oracle.get_transp_state (oracle env)
-      else TranspState.full
+      else TransparentState.full
     in
     let flags =
       if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
@@ -4909,7 +4909,7 @@ let constr_eq ~strict x y =
       | None -> fail
   end
 
-let unify ?(state=TranspState.full) x y =
+let unify ?(state=TransparentState.full) x y =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -4922,7 +4922,7 @@ let unify ?(state=TranspState.full) x y =
     let flags = { (default_unify_flags ()) with
       core_unify_flags = core_flags;
       merge_unify_flags = core_flags;
-      subterm_unify_flags = { core_flags with modulo_delta = TranspState.empty } }
+      subterm_unify_flags = { core_flags with modulo_delta = TransparentState.empty } }
     in
     let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in
     Proofview.Unsafe.tclEVARS sigma
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 1db65fc1aa..4e91a9a728 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -419,7 +419,7 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
    are added to the evar map. *)
 val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic
 
-val unify           : ?state:TranspState.t -> constr -> constr -> unit Proofview.tactic
+val unify           : ?state:TransparentState.t -> constr -> constr -> unit Proofview.tactic
 
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
 val specialize_eqs : Id.t -> unit Proofview.tactic
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index b51b6cedfb..3ca2a4ad6b 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -315,7 +315,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
       let t = type_of_constant cb in
       let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
       ContextObjectMap.add (Axiom (Constant kn,l)) t accu
-    else if add_opaque && (Declareops.is_opaque cb || not (TranspState.is_transparent_constant st kn)) then
+    else if add_opaque && (Declareops.is_opaque cb || not (TransparentState.is_transparent_constant st kn)) then
       let t = type_of_constant cb in
       ContextObjectMap.add (Opaque kn) t accu
     else if add_transparent then
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 56d6202194..536185f4aa 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -28,5 +28,5 @@ val traverse :
    on which a term relies (together with their type). The above warning of
    {!traverse} also applies. *)
 val assumptions :
-  ?add_opaque:bool -> ?add_transparent:bool -> TranspState.t ->
+  ?add_opaque:bool -> ?add_transparent:bool -> TransparentState.t ->
      GlobRef.t -> constr -> types ContextObjectMap.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 34ddf3377f..7765f5b417 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1096,7 +1096,7 @@ let vernac_restore_state file =
 (* Commands *)
 
 let vernac_create_hintdb ~module_local id b =
-  Hints.create_hint_db module_local id TranspState.full b
+  Hints.create_hint_db module_local id TransparentState.full b
 
 let vernac_remove_hints ~module_local dbs ids =
   Hints.remove_hints module_local dbs (List.map Smartlocate.global_with_alias ids)