Rename TranspState into TransparentState.

10 files changed, 21 insertions, 21 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 625a9a7277..7e73609996 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -72,8 +72,8 @@ let with_stats c =
   end else
     Lazy.force c
 
-let all_opaque = TranspState.empty
-let all_transparent = TranspState.full
+let all_opaque = TransparentState.empty
+let all_transparent = TransparentState.full
 
 module type RedFlagsSig = sig
   type reds
@@ -90,8 +90,8 @@ module type RedFlagsSig = sig
   val no_red : reds
   val red_add : reds -> red_kind -> reds
   val red_sub : reds -> red_kind -> reds
-  val red_add_transparent : reds -> TranspState.t -> reds
-  val red_transparent : reds -> TranspState.t
+  val red_add_transparent : reds -> TransparentState.t -> reds
+  val red_transparent : reds -> TransparentState.t
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
   val red_projection : reds -> Projection.t -> bool
@@ -103,13 +103,13 @@ module RedFlags = (struct
   (* [r_const=(false,cl)] means only those in [cl] *)
   (* [r_delta=true] just mean [r_const=(true,[])] *)
 
-  open TranspState
+  open TransparentState
 
   type reds = {
     r_beta : bool;
     r_delta : bool;
     r_eta : bool;
-    r_const : TranspState.t;
+    r_const : TransparentState.t;
     r_zeta : bool;
     r_match : bool;
     r_fix : bool;
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 26710a64d0..b6c87b3732 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -52,10 +52,10 @@ module type RedFlagsSig = sig
   val red_sub : reds -> red_kind -> reds
 
   (** Adds a reduction kind to a set *)
-  val red_add_transparent : reds -> TranspState.t -> reds
+  val red_add_transparent : reds -> TransparentState.t -> reds
 
   (** Retrieve the transparent state of the reduction flags *)
-  val red_transparent : reds -> TranspState.t
+  val red_transparent : reds -> TransparentState.t
 
   (** Build a reduction set from scratch = iter [red_add] on [no_red] *)
   val mkflags : red_kind list -> reds
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index c66beb49b8..fe82353b70 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -82,7 +82,7 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu =
   Cmap.fold fcst cst_opacity accu
 
 let get_transp_state { var_trstate; cst_trstate; _ } =
-  { TranspState.tr_var = var_trstate; tr_cst = cst_trstate }
+  { TransparentState.tr_var = var_trstate; tr_cst = cst_trstate }
 
 let dep_order l2r k1 k2 = match k1, k2 with
 | RelKey _, RelKey _ -> l2r
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 3b51515352..bc06cc21b6 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -41,5 +41,5 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle
 (** Fold over the non-transparent levels of the oracle. Order unspecified. *)
 val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a
 
-val get_transp_state : oracle -> TranspState.t
+val get_transp_state : oracle -> TransparentState.t
 
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index e716972ebe..54c239349d 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,5 +1,5 @@
 Names
-TranspState
+TransparentState
 Uint31
 Univ
 UGraph
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a45a5b3247..fbb481424f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -177,7 +177,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
 
 (* functions of this type can be called from outside the kernel *)
 type 'a extended_conversion_function =
-  ?l2r:bool -> ?reds:TranspState.t -> env ->
+  ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:((existential->constr option) * UGraph.t) ->
   'a -> 'a -> unit
 
@@ -758,7 +758,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
 	()
 
 (* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=TranspState.full) env ?(evars=(fun _->None), universes env) =
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) =
   let evars, univs = evars in
   if Flags.profile then
     let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
@@ -792,11 +792,11 @@ let infer_conv_universes =
       CProfile.profile8 infer_conv_universes_key infer_conv_universes
   else infer_conv_universes
 
-let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full)
+let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
     env univs t1 t2 = 
   infer_conv_universes CONV l2r evars ts env univs t1 t2
 
-let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full)
+let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
     env univs t1 t2 = 
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 9b26e7b3dc..0408dbf057 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -31,7 +31,7 @@ exception NotConvertibleVect of int
 
 type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
 type 'a extended_conversion_function = 
-  ?l2r:bool -> ?reds:TranspState.t -> env ->
+  ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:((existential->constr option) * UGraph.t) ->
   'a -> 'a -> unit
 
@@ -77,15 +77,15 @@ val conv_leq : types extended_conversion_function
 (** These conversion functions are used by module subtyping, which needs to infer
     universe constraints inside the kernel *)
 val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> 
-  ?ts:TranspState.t -> constr infer_conversion_function
+  ?ts:TransparentState.t -> constr infer_conversion_function
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
-  ?ts:TranspState.t -> types infer_conversion_function
+  ?ts:TransparentState.t -> types infer_conversion_function
 
 (** Depending on the universe state functions, this might raise
   [UniverseInconsistency] in addition to [NotConvertible] (for better error
   messages). *)
 val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
-  TranspState.t -> (constr,'a) generic_conversion_function
+  TransparentState.t -> (constr,'a) generic_conversion_function
 
 val default_conv     : conv_pb -> ?l2r:bool -> types kernel_conversion_function
 val default_conv_leq : ?l2r:bool -> types kernel_conversion_function
diff --git a/kernel/transpState.ml b/kernel/transparentState.ml
index 9661dace6a..9661dace6a 100644
--- a/kernel/transpState.ml
+++ b/kernel/transparentState.ml
diff --git a/kernel/transpState.mli b/kernel/transparentState.mli
index f2999c6869..f2999c6869 100644
--- a/kernel/transpState.mli
+++ b/kernel/transparentState.mli
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 46e52121c7..246c90c09d 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -191,7 +191,7 @@ let warn_bytecode_compiler_failed =
 let vm_conv_gen cv_pb env univs t1 t2 =
   if not (typing_flags env).Declarations.enable_VM then
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TranspState.full env univs t1 t2
+      TransparentState.full env univs t1 t2
   else
   try
     let v1 = val_of_constr env t1 in
@@ -200,7 +200,7 @@ let vm_conv_gen cv_pb env univs t1 t2 =
   with Not_found | Invalid_argument _ ->
     warn_bytecode_compiler_failed ();
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TranspState.full env univs t1 t2
+      TransparentState.full env univs t1 t2
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in