Merge PR #7925: Clean transparent state

49 files changed, 298 insertions, 252 deletions

diff --git a/checker/dune b/checker/dune
index 35a35a1f82..3ab4f50d13 100644
--- a/checker/dune
+++ b/checker/dune
@@ -14,7 +14,7 @@
   %{project_root}/kernel/{cbytegen,clambda,nativeinstr,nativevalues,nativeconv,nativecode,nativelib,nativelibrary,nativelambda}.ml{,i})
 
 (copy_files#
-  %{project_root}/kernel/{subtyping,term_typing,safe_typing,entries,cooking}.ml{,i})
+  %{project_root}/kernel/{subtyping,term_typing,safe_typing,entries,cooking,transparentState}.ml{,i})
 
 ; VM stuff
 
diff --git a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh
new file mode 100644
index 0000000000..b05d02c5be
--- /dev/null
+++ b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh
@@ -0,0 +1,14 @@
+_OVERLAY_BRANCH=clean-transp-state
+
+if [ "$CI_PULL_REQUEST" = "7925" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
+
+    unicoq_CI_REF="$_OVERLAY_BRANCH"
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+    equations_CI_REF="$_OVERLAY_BRANCH"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    mtac2_CI_REF="$_OVERLAY_BRANCH"
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index b1fdfafd3a..30a2967259 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -19,6 +19,10 @@ 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 `TransparentState`.
+  This module gathers utility functions that used to be defined in several
+  places.
+
 Coqlib:
 
 - Most functions from the `Coqlib` module have been deprecated in favor of
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 63d7d58053..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 : Names.transparent_state -> 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 95546a83e1..7e73609996 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -72,11 +72,8 @@ let with_stats c =
   end else
     Lazy.force c
 
-let all_opaque = (Id.Pred.empty, Cpred.empty)
-let all_transparent = (Id.Pred.full, Cpred.full)
-
-let is_transparent_variable (ids, _) id = Id.Pred.mem id ids
-let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
+let all_opaque = TransparentState.empty
+let all_transparent = TransparentState.full
 
 module type RedFlagsSig = sig
   type reds
@@ -93,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 -> transparent_state -> reds
-  val red_transparent : reds -> transparent_state
+  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
@@ -106,11 +103,13 @@ module RedFlags = (struct
   (* [r_const=(false,cl)] means only those in [cl] *)
   (* [r_delta=true] just mean [r_const=(true,[])] *)
 
+  open TransparentState
+
   type reds = {
     r_beta : bool;
     r_delta : bool;
     r_eta : bool;
-    r_const : transparent_state;
+    r_const : TransparentState.t;
     r_zeta : bool;
     r_match : bool;
     r_fix : bool;
@@ -143,30 +142,30 @@ module RedFlags = (struct
     | ETA -> { red with r_eta = true }
     | DELTA -> { red with r_delta = true; r_const = all_transparent }
     | CONST kn ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, Cpred.add kn l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_cst = Cpred.add kn r.tr_cst } }
     | MATCH -> { red with r_match = true }
     | FIX -> { red with r_fix = true }
     | COFIX -> { red with r_cofix = true }
     | ZETA -> { red with r_zeta = true }
     | VAR id ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = Id.Pred.add id l1, l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_var = Id.Pred.add id r.tr_var } }
 
   let red_sub red = function
     | BETA -> { red with r_beta = false }
     | ETA -> { red with r_eta = false }
     | DELTA -> { red with r_delta = false }
     | CONST kn ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, Cpred.remove kn l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_cst = Cpred.remove kn r.tr_cst } }
     | MATCH -> { red with r_match = false }
     | FIX -> { red with r_fix = false }
     | COFIX -> { red with r_cofix = false }
     | ZETA -> { red with r_zeta = false }
     | VAR id ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = Id.Pred.remove id l1, l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_var = Id.Pred.remove id r.tr_var } }
 
   let red_transparent red = red.r_const
 
@@ -179,12 +178,10 @@ module RedFlags = (struct
     | BETA -> incr_cnt red.r_beta beta
     | ETA -> incr_cnt red.r_eta eta
     | CONST kn ->
-	let (_,l) = red.r_const in
-	let c = Cpred.mem kn l in
+      let c = is_transparent_constant red.r_const kn in
 	incr_cnt c delta
     | VAR id -> (* En attendant d'avoir des kn pour les Var *)
-	let (l,_) = red.r_const in
-	let c = Id.Pred.mem id l in
+      let c = is_transparent_variable red.r_const id in
 	incr_cnt c delta
     | ZETA -> incr_cnt red.r_zeta zeta
     | MATCH -> incr_cnt red.r_match nb_match
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 1ee4bccc25..b6c87b3732 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -24,14 +24,6 @@ val with_stats: 'a Lazy.t -> 'a
   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
   a LetIn expression is Letin reduction *)
 
-
-
-val all_opaque      : transparent_state
-val all_transparent : transparent_state
-
-val is_transparent_variable : transparent_state -> variable -> bool
-val is_transparent_constant : transparent_state -> Constant.t -> bool
-
 (** Sets of reduction kinds. *)
 module type RedFlagsSig = sig
   type reds
@@ -60,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 -> transparent_state -> reds
+  val red_add_transparent : reds -> TransparentState.t -> reds
 
   (** Retrieve the transparent state of the reduction flags *)
-  val red_transparent : reds -> transparent_state
+  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 ac78064235..fe82353b70 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -81,7 +81,8 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu =
   let accu = Id.Map.fold fvar var_opacity accu in
   Cmap.fold fcst cst_opacity accu
 
-let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate)
+let get_transp_state { var_trstate; 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 67add5dd35..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 -> transparent_state
+val get_transp_state : oracle -> TransparentState.t
 
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index a18c5d1e20..54c239349d 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,4 +1,5 @@
 Names
+TransparentState
 Uint31
 Univ
 UGraph
diff --git a/kernel/names.ml b/kernel/names.ml
index 18560d5f8d..b2d6a489a6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -715,13 +715,6 @@ let hcons_construct = Hashcons.simple_hcons Hconstruct.generate Hconstruct.hcons
 
 (*****************)
 
-type transparent_state = Id.Pred.t * Cpred.t
-
-let empty_transparent_state = (Id.Pred.empty, Cpred.empty)
-let full_transparent_state = (Id.Pred.full, Cpred.full)
-let var_full_transparent_state = (Id.Pred.full, Cpred.empty)
-let cst_full_transparent_state = (Id.Pred.empty, Cpred.full)
-
 type 'a tableKey =
   | ConstKey of 'a
   | VarKey of Id.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 98995752a2..350db871d5 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -510,14 +510,6 @@ type 'a tableKey =
   | VarKey of Id.t
   | RelKey of Int.t
 
-(** Sets of names *)
-type transparent_state = Id.Pred.t * Cpred.t
-
-val empty_transparent_state : transparent_state
-val full_transparent_state : transparent_state
-val var_full_transparent_state : transparent_state
-val cst_full_transparent_state : transparent_state
-
 type inv_rel_key = int (** index in the [rel_context] part of environment
 			  starting by the end, {e inverse}
 			  of de Bruijn indice *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5515ff9767..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:Names.transparent_state -> 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=full_transparent_state) 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=full_transparent_state)
+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=full_transparent_state) 
+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 581e8bd88a..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:Names.transparent_state -> 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:Names.transparent_state -> constr infer_conversion_function
+  ?ts:TransparentState.t -> constr infer_conversion_function
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
-  ?ts:Names.transparent_state -> 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) ->
-  Names.transparent_state -> (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/transparentState.ml b/kernel/transparentState.ml
new file mode 100644
index 0000000000..9661dace6a
--- /dev/null
+++ b/kernel/transparentState.ml
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+type t = {
+  tr_var : Id.Pred.t;
+  tr_cst : Cpred.t;
+}
+
+let empty = {
+  tr_var = Id.Pred.empty;
+  tr_cst = Cpred.empty;
+}
+
+let full = {
+  tr_var = Id.Pred.full;
+  tr_cst = Cpred.full;
+}
+
+let var_full = {
+  tr_var = Id.Pred.full;
+  tr_cst = Cpred.empty;
+}
+
+let cst_full = {
+  tr_var = Id.Pred.empty;
+  tr_cst = Cpred.full;
+}
+
+let is_empty ts =
+  Id.Pred.is_empty ts.tr_var && Cpred.is_empty ts.tr_cst
+
+let is_transparent_variable ts id =
+  Id.Pred.mem id ts.tr_var
+
+let is_transparent_constant ts cst =
+  Cpred.mem cst ts.tr_cst
diff --git a/kernel/transparentState.mli b/kernel/transparentState.mli
new file mode 100644
index 0000000000..f2999c6869
--- /dev/null
+++ b/kernel/transparentState.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(** Sets of names *)
+type t = {
+  tr_var : Id.Pred.t;
+  tr_cst : Cpred.t;
+}
+
+val empty : t
+(** Everything opaque *)
+
+val full : t
+(** Everything transparent *)
+
+val var_full : t
+(** All variables transparent *)
+
+val cst_full : t
+(** All constant transparent *)
+
+val is_empty : t -> bool
+
+val is_transparent_variable : t -> Id.t -> bool
+val is_transparent_constant : t -> Constant.t -> bool
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index c1130e62c9..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)
-      full_transparent_state 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)
-      full_transparent_state 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 516b04ea21..6a80525200 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -18,16 +18,16 @@ open Tacticals.New
 open Globnames
 
 let update_flags ()=
-  let f acc coe =
-    match coe.Classops.coe_value with
-    | ConstRef c -> Names.Cpred.add c acc
-    | _ -> acc
+  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 pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in
+  let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in
     red_flags:=
     CClosure.RedFlags.red_add_transparent
       CClosure.betaiotazeta
-      (Names.Id.Pred.full,Names.Cpred.complement pred)
+      flags
 
 let ground_tac solver startseq =
   Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 651895aa08..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 empty_transparent_state false]
+                                      [Hints.Hint_db.empty TransparentState.empty false]
 				  )
 			   )
 			)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 63a3e0582d..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 empty_transparent_state false]
+                        [Hints.Hint_db.empty TransparentState.empty false]
 		      ]
 		    )
 		  )
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 16cb75ea2f..fee469032c 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 = 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 = empty_transparent_state;
-  Unification.modulo_delta_types = full_transparent_state;
+  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 = full_transparent_state;
+      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 = empty_transparent_state };
+    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 164f5ab96d..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 full_transparent_state) !!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 6a75be352b..f370ad7ae2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -16,7 +16,6 @@ open Termops
 open Environ
 open EConstr
 open Vars
-open CClosure
 open Reduction
 open Reductionops
 open Recordops
@@ -30,7 +29,7 @@ open Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-type unify_fun = transparent_state ->
+type unify_fun = TransparentState.t ->
   env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
 
 let debug_unification = ref (false)
@@ -74,14 +73,14 @@ let coq_unit_judge =
 
 let unfold_projection env evd ts p c =
   let cst = Projection.constant p in
-    if 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 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 ->
@@ -91,7 +90,7 @@ let eval_flexible_term ts env evd c =
        with Not_found -> None)
   | Var id ->
       (try
-	 if 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)
@@ -1211,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 full_transparent_state)
+            (evar_conv_x TransparentState.full)
       with IllTypedInstance _ -> raise (TypingFailed evd)
     in
       Evd.define evk rhs evd
@@ -1354,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 full_transparent_state 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
@@ -1393,7 +1392,7 @@ let solve_unif_constraints_with_heuristics env
 
 exception UnableToUnify of evar_map * unification_error
 
-let default_transparent_state env = full_transparent_state
+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 350dece28a..4585fac252 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Names
 open EConstr
 open Environ
 open Reductionops
@@ -22,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:transparent_state -> constr -> constr -> evar_map -> evar_map
-val the_conv_x_leq : env -> ?ts:transparent_state -> 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:transparent_state -> evar_map -> constr -> constr -> evar_map option
-val cumul : env -> ?ts:transparent_state -> 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:transparent_state -> 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 *)
@@ -55,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 : transparent_state -> 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 = transparent_state ->
+type unify_fun = TransparentState.t ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
 
 (** Override default [evar_conv_x] algorithm. *)
@@ -73,7 +72,7 @@ val evar_conv_x : unify_fun
 
 (**/**)
 (* For debugging *)
-val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * 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 17003cd1dd..e632976ae5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -675,10 +675,6 @@ let apply_subst recfun env sigma refold cst_l t stack =
 let stacklam recfun env sigma t stack =
   apply_subst (fun _ _ s -> recfun s) env sigma false Cst_stack.empty t stack
 
-let beta_app sigma (c,l) =
-  let zip s = Stack.zip sigma s in
-  stacklam zip [] sigma c (Stack.append_app l Stack.empty)
-
 let beta_applist sigma (c,l) =
   let zip s = Stack.zip sigma s in
   stacklam zip [] sigma c (Stack.append_app_list l Stack.empty)
@@ -1305,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=full_transparent_state) env sigma = test_trans_conversion f_conv reds env sigma
-let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv_leq reds env sigma
-let is_fconv ?(reds=full_transparent_state) = 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=full_transparent_state) 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
@@ -1345,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=full_transparent_state) env sigma x y =
+    ?(ts=TransparentState.full) env sigma x y =
   (** FIXME *)
   try
       let ans = match pb with
@@ -1378,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:full_transparent_state)
+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
@@ -1681,25 +1677,6 @@ let meta_reducible_instance evd b =
   if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
   else irec b.rebus
 
-
-let head_unfold_under_prod ts env sigma c =
-  let unfold (cst,u) =
-    let cstu = (cst, EInstance.kind sigma u) in
-    if Cpred.mem cst (snd ts) then
-      match constant_opt_value_in env cstu with
-	| Some c -> EConstr.of_constr c
-	| None -> mkConstU (cst, u)
-    else mkConstU (cst, u) in
-  let rec aux c =
-    match EConstr.kind sigma c with
-      | Prod (n,t,c) -> mkProd (n,aux t, aux c)
-      | _ ->
-	  let (h,l) = decompose_app_vect sigma c in
-	  match EConstr.kind sigma h with
-	    | Const cst -> beta_app sigma (unfold cst, l)
-	    | _ -> c in
-  aux c
-
 let betazetaevar_applist sigma n c l =
   let rec stacklam n env t stack =
     if Int.equal n 0 then applist (substl env t, stack) else
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 41de779414..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:transparent_state -> env -> evar_map -> constr -> constr -> bool
-val is_conv_leq : ?reds:transparent_state -> env ->  evar_map -> constr -> constr -> bool
-val is_fconv : ?reds:transparent_state -> 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:transparent_state -> 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:transparent_state -> 
+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 -> transparent_state ->
+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:transparent_state -> env ->
+  ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env ->
   evar_map -> constr -> constr -> evar_map option
 
 (** {6 Special-Purpose Reduction Functions } *)
@@ -302,13 +302,12 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
 val whd_meta : local_reduction_function
 val plain_instance : evar_map -> constr Metamap.t -> constr -> constr
 val instance : evar_map -> constr Metamap.t -> constr -> constr
-val head_unfold_under_prod : transparent_state -> reduction_function
 val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
 
 (** {6 Heuristic for Conversion with Evar } *)
 
 val whd_betaiota_deltazeta_for_iota_state :
-  transparent_state -> 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/tacred.ml b/pretyping/tacred.ml
index 4ec8569dd8..d9df8c8cf8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -638,7 +638,7 @@ let whd_nothing_for_iota env sigma s =
       | Meta ev ->
         (try whrec (Evd.meta_value sigma ev, stack)
 	with Not_found -> s)
-      | Const (const, u) when is_transparent_constant full_transparent_state const ->
+      | Const (const, u) ->
           let u = EInstance.kind sigma u in
 	  (match constant_opt_value_in env (const, u) with
 	     | Some  body -> whrec (EConstr.of_constr body, stack)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ee9c83dad3..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 -> transparent_state) Hook.t
-val classes_transparent_state : unit -> transparent_state
+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 e3b942b610..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 empty_transparent_state
+    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 : Names.transparent_state 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 : Names.transparent_state;
+  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 : Names.transparent_state;
+  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 = Names.full_transparent_state 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 = var_full_transparent_state };
+  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 = empty_transparent_state;
+  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 = empty_transparent_state;
+  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 = empty_transparent_state;
+  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 = empty_transparent_state };
+  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 = empty_transparent_state;
+  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) &&
-      (Cpred.mem cst (snd flags.modulo_delta)
+      (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) && 
-      Id.Pred.mem id (fst flags.modulo_delta) ->
+      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)) &&
-       (Cpred.mem (Projection.constant p) (snd flags.modulo_delta))) ->
+       (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 (Cpred.mem cst (snd flags.modulo_delta))
+  | 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 (Cpred.mem c (snd ts))
+      not (TransparentState.is_transparent_constant ts c)
     | Var id -> 
       not (Environ.evaluable_named id env) ||
       not (is_transparent env (VarKey id)) ||
-      not (Id.Pred.mem id (fst ts))
+      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 full_transparent_state;
-	      modulo_delta = full_transparent_state;
+            { flags with modulo_conv_on_closed_terms = Some TransparentState.full;
+              modulo_delta = TransparentState.full;
 	      modulo_eta = true;
 	      modulo_betaiota = true }
 	    ty1 ty2
@@ -1120,10 +1120,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       | Some sigma -> ans
       | None ->
         if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
-        | Some (cv_id, cv_k), (dl_id, dl_k) ->
-          Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
-        | None,(dl_id, dl_k) ->
-          Id.Pred.is_empty dl_id && Cpred.is_empty dl_k)
+        | Some cv, dl ->
+          let open TransparentState in
+          Id.Pred.subset dl.tr_var cv.tr_var && Cpred.subset dl.tr_cst cv.tr_cst
+        | 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 (CClosure.is_transparent_constant ts c)
-  | Var id -> not (CClosure.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 = Names.full_transparent_state in {
-  modulo_conv_on_closed_terms = Some empty_transparent_state;
+  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 = empty_transparent_state;
+  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 = Names.full_transparent_state 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 Names.full_transparent_state;
+        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 e2e261ae7a..a45b8f1dd8 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -8,18 +8,17 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Names
 open Constr
 open EConstr
 open Environ
 open Evd
 
 type core_unify_flags = {
-  modulo_conv_on_closed_terms : Names.transparent_state 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 : Names.transparent_state;
-  modulo_delta_types : Names.transparent_state;
+  modulo_delta : TransparentState.t;
+  modulo_delta_types : TransparentState.t;
   check_applied_meta_types : bool;
   use_pattern_unification : bool;
   use_meta_bound_pattern_unification : bool;
@@ -41,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 : transparent_state -> 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 7ce08ed6bc..831008a957 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -456,9 +456,9 @@ let pr_predicate pr_elt (b, elts) =
 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 (ids, csts) =
-  hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
-	str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
+let pr_transparent_state ts =
+  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 e50b02b508..785f452a7b 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -135,7 +135,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   : transparent_state -> 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 b99cf245fe..c7703b52c7 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Util
-open Names
 open Constr
 open Termops
 open Evd
@@ -102,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 full_transparent_state;
+  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 = empty_transparent_state;
-  modulo_delta_types = full_transparent_state;
+  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 cb71f09826..6c4193c66b 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -10,7 +10,6 @@
 
 open CErrors
 open Util
-open Names
 open Evd
 open Evarutil
 open Evarsolve
@@ -38,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 full_transparent_state 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 56ce744bc1..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) all_opaque 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 65b2615b6b..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 = full_transparent_state;
+  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 = empty_transparent_state };
+  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 full_transparent_state empty_transparent_state
+  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 full_transparent_state st
+  auto_unif_flags_of TransparentState.full st
 
 let hintmap_of sigma secvars hdc concl =
   match hdc with
@@ -358,12 +358,12 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 	  let flags = flags_of_state (Hint_db.transparent_state db) in
 	    List.map (fun x -> (Some flags, x)) (f db)
 	else
-	  let (ids, csts as st) = Hint_db.transparent_state db in
+          let st = Hint_db.transparent_state db in
 	  let flags, l =
 	    let l =
 	      match hdc with None -> Hint_db.map_none ~secvars db
 	      | Some hdc ->
-		  if (Id.Pred.is_empty ids && Cpred.is_empty csts)
+                  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 a835c1ed95..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 : transparent_state -> 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 bfee0422e7..2f2bd8d2bc 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -69,13 +69,13 @@ let constr_pat_discr t =
     | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args)
     | _ -> None
 
-let constr_val_discr_st sigma (idpred,cpred) 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 Cpred.mem c cpred 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 (Id.Pred.mem id idpred) -> 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 
@@ -85,15 +85,15 @@ let constr_val_discr_st sigma (idpred,cpred) t =
     | Evar _ -> Everything
     | _ -> Nothing
 
-let constr_pat_discr_st (idpred,cpred) t =
+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 (Id.Pred.mem v idpred) ->
+  | PRef ((VarRef v) as ref), args when not (TransparentState.is_transparent_variable ts v) ->
       Some(GRLabel ref,args)
-  | PVar v, args when not (Id.Pred.mem v idpred) ->
+  | PVar v, args when not (TransparentState.is_transparent_variable ts v) ->
       Some(GRLabel (VarRef v),args)
-  | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) ->
+  | 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 861c9b6250..cc31fb0599 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Pattern
-open Names
 
 (** Discrimination nets with bounded depth. *)
 
@@ -19,7 +18,7 @@ open Names
 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 [transparent_state]
+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]. *)
@@ -31,10 +30,10 @@ sig
 
   val empty : t
 
-  val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t
-  val rmv : transparent_state 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 -> transparent_state 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 81cf9289d1..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 full_transparent_state true)
+       Hint_db.empty TransparentState.full true)
 
-  let make_autogoal_hints only_classes ?(st=full_transparent_state) 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=full_transparent_state) 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=full_transparent_state) 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=full_transparent_state) ?(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=full_transparent_state)
+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 9ba69a0584..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:transparent_state -> ?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:Names.transparent_state ->
+    ?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 5067315d08..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 full_transparent_state
+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:full_transparent_state 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:full_transparent_state 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 c4a6b1605d..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 = empty_transparent_state;
-  modulo_delta_types = empty_transparent_state;
+  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 full_transparent_state;
+  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 = empty_transparent_state;
-  modulo_delta_types = full_transparent_state;
+  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 full_transparent_state;
+  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 = full_transparent_state;
-  modulo_delta_types = full_transparent_state;
+  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 328d57c8a3..e64e08dbde 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -290,9 +290,9 @@ let lookup_tacs sigma concl st se =
 
 module Constr_map = Map.Make(GlobRef.Ordered)
 
-let is_transparent_gr (ids, csts) = function
-  | VarRef id -> Id.Pred.mem id ids
-  | ConstRef cst -> Cpred.mem cst csts
+let is_transparent_gr ts = function
+  | 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 -> transparent_state -> 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 -> transparent_state
-val set_transparent_state : t -> transparent_state -> 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 : Names.transparent_state;
+    hintdb_state : TransparentState.t;
     hintdb_cut : hints_path;
     hintdb_unfolds : Id.Set.t * Cset.t;
     hintdb_max_id : int;
@@ -663,10 +663,13 @@ struct
     let st',db,rebuild =
       match v.code.obj with
       | Unfold_nth egr ->
-	  let addunf (ids,csts) (ids',csts') =
+          let addunf ts (ids, csts) =
+            let open TransparentState in
 	    match egr with
-	    | EvalVarRef id -> (Id.Pred.add id ids, csts), (Id.Set.add id ids', csts')
-	    | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts')
+            | EvalVarRef id ->
+              { ts with tr_var = Id.Pred.add id ts.tr_var }, (Id.Set.add id ids, csts)
+            | EvalConstRef cst ->
+              { ts with tr_cst = Cpred.add cst ts.tr_cst }, (ids, Cset.add cst csts)
 	  in 
 	  let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
 	    state, { db with hintdb_unfolds = unfs }, true
@@ -740,8 +743,8 @@ let typeclasses_db = "typeclass_instances"
 let rewrite_db = "rewrite"
 
 let auto_init_db =
-  Hintdbmap.add typeclasses_db (Hint_db.empty full_transparent_state true)
-    (Hintdbmap.add rewrite_db (Hint_db.empty cst_full_transparent_state 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
@@ -977,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 empty_transparent_state false
+  with Not_found -> Hint_db.empty ~name:dbname TransparentState.empty false
 
 let add_hint dbname hintlist =
   let check (_, h) =
@@ -995,18 +998,19 @@ let add_hint dbname hintlist =
     searchtable_add (dbname,db')
 
 let add_transparency dbname target b =
+  let open TransparentState in
   let db = get_db dbname in
-  let (ids, csts as st) = Hint_db.transparent_state db in
+  let st = Hint_db.transparent_state db in
   let st' =
     match target with
-    | HintsVariables -> (if b then Id.Pred.full else Id.Pred.empty), csts
-    | HintsConstants -> ids, if b then Cpred.full else Cpred.empty
+    | HintsVariables -> { st with tr_var = (if b then Id.Pred.full else Id.Pred.empty) }
+    | HintsConstants -> { st with tr_cst = (if b then Cpred.full else Cpred.empty) }
     | HintsReferences grs ->
-       List.fold_left (fun (ids, csts) gr ->
-       match gr with
-       | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts)
-       | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts)
-                      st grs
+      List.fold_left (fun st gr ->
+        match gr with
+        | EvalConstRef c -> { st with tr_cst = (if b then Cpred.add else Cpred.remove) c st.tr_cst }
+        | EvalVarRef v -> { st with tr_var = (if b then Id.Pred.add else Id.Pred.remove) v st.tr_var })
+        st grs
   in searchtable_add (dbname, Hint_db.set_transparent_state db st')
 
 let remove_hint dbname grs =
@@ -1015,7 +1019,7 @@ let remove_hint dbname grs =
     searchtable_add (dbname, db')
 
 type hint_action =
-  | CreateDB of bool * transparent_state
+  | CreateDB of bool * TransparentState.t
   | AddTransparency of evaluable_global_reference hints_transparency_target * bool
   | AddHints of hint_entry list
   | RemoveHints of GlobRef.t list
@@ -1543,7 +1547,7 @@ let pr_hint_db_env env sigma db =
     in
     Hint_db.fold fold db (mt ())
   in
-  let (ids, 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 6db8feccd0..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 -> transparent_state -> 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 -> transparent_state
-    val set_transparent_state : t -> transparent_state -> 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 -> transparent_state -> 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:transparent_state -> 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 03ad1b4c4f..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 full_transparent_state
+      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 full_transparent_state
+      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=full_transparent_state) 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=full_transparent_state) 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 = empty_transparent_state } }
+      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 b298524ff8..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:Names.transparent_state -> 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 6beac2032d..3ca2a4ad6b 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -294,7 +294,6 @@ let traverse current t =
 let type_of_constant cb = cb.Declarations.const_type
 
 let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
-  let (idts, knst) = st in
   (** Only keep the transitive dependencies *)
   let (_, graph, ax2ty) = traverse (label_of gr) t in
   let fold obj _ accu = match obj with
@@ -316,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 (Cpred.mem kn knst)) 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 aead345d8c..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 -> transparent_state ->
+  ?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 0405e4f27c..df4193f397 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 full_transparent_state b
+  Hints.create_hint_db module_local id TransparentState.full b
 
 let warn_implicit_core_hint_db =
   CWarnings.create ~name:"implicit-core-hint-db" ~category:"deprecated"