Rename TranspState into TransparentState.

8 files changed, 64 insertions, 64 deletions

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