Move transparent_state to its own module.

11 files changed, 65 insertions, 35 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 95546a83e1..c8028f713a 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -93,8 +93,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 -> TranspState.t -> reds
+  val red_transparent : reds -> TranspState.t
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
   val red_projection : reds -> Projection.t -> bool
@@ -110,7 +110,7 @@ module RedFlags = (struct
     r_beta : bool;
     r_delta : bool;
     r_eta : bool;
-    r_const : transparent_state;
+    r_const : TranspState.t;
     r_zeta : bool;
     r_match : bool;
     r_fix : bool;
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 1ee4bccc25..9d41ee0695 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -26,11 +26,11 @@ val with_stats: 'a Lazy.t -> 'a
 
 
 
-val all_opaque      : transparent_state
-val all_transparent : transparent_state
+val all_opaque      : TranspState.t
+val all_transparent : TranspState.t
 
-val is_transparent_variable : transparent_state -> variable -> bool
-val is_transparent_constant : transparent_state -> Constant.t -> bool
+val is_transparent_variable : TranspState.t -> variable -> bool
+val is_transparent_constant : TranspState.t -> Constant.t -> bool
 
 (** Sets of reduction kinds. *)
 module type RedFlagsSig = sig
@@ -60,10 +60,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 -> TranspState.t -> reds
 
   (** Retrieve the transparent state of the reduction flags *)
-  val red_transparent : reds -> transparent_state
+  val red_transparent : reds -> TranspState.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.mli b/kernel/conv_oracle.mli
index 67add5dd35..3b51515352 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 -> TranspState.t
 
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index a18c5d1e20..e716972ebe 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,4 +1,5 @@
 Names
+TranspState
 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..a45a5b3247 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:TranspState.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=TranspState.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=TranspState.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=TranspState.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..9b26e7b3dc 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:TranspState.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:TranspState.t -> constr infer_conversion_function
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
-  ?ts:Names.transparent_state -> types infer_conversion_function
+  ?ts:TranspState.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
+  TranspState.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/transpState.ml
new file mode 100644
index 0000000000..9acb7244f7
--- /dev/null
+++ b/kernel/transpState.ml
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*         *   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 = Id.Pred.t * Cpred.t
+
+let empty = (Id.Pred.empty, Cpred.empty)
+let full = (Id.Pred.full, Cpred.full)
+let var_full = (Id.Pred.full, Cpred.empty)
+let cst_full = (Id.Pred.empty, Cpred.full)
diff --git a/kernel/transpState.mli b/kernel/transpState.mli
new file mode 100644
index 0000000000..a8d301549b
--- /dev/null
+++ b/kernel/transpState.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   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 = Id.Pred.t * 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 *)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index c1130e62c9..46e52121c7 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
+      TranspState.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
+      TranspState.full env univs t1 t2
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in