Move transparent_state to its own module.

9 files changed, 53 insertions, 55 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 164f5ab96d..647ef5092f 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 TranspState.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..68b53787f9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -30,7 +30,7 @@ open Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-type unify_fun = transparent_state ->
+type unify_fun = TranspState.t ->
   env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
 
 let debug_unification = ref (false)
@@ -1211,7 +1211,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 TranspState.full)
       with IllTypedInstance _ -> raise (TypingFailed evd)
     in
       Evd.define evk rhs evd
@@ -1354,7 +1354,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 TranspState.full in
       let evd' = check_evar_instance evd' evk ty conv_algo in
         Evd.define evk ty evd'
     | _ -> evd') evd evd
@@ -1393,7 +1393,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 = TranspState.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..721a6fad8e 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:TranspState.t -> constr -> constr -> evar_map -> evar_map
+val the_conv_x_leq : env -> ?ts:TranspState.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:TranspState.t -> evar_map -> constr -> constr -> evar_map option
+val cumul : env -> ?ts:TranspState.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:TranspState.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 : TranspState.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 = TranspState.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 -> TranspState.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..18b0bab892 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1305,13 +1305,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=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
   | 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=TranspState.full) env sigma x y =
   let f = match pb with
     | Reduction.CONV -> f_conv
     | Reduction.CUMUL -> f_conv_leq
@@ -1345,7 +1345,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=TranspState.full) env sigma x y =
   (** FIXME *)
   try
       let ans = match pb with
@@ -1378,7 +1378,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:TranspState.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 41de779414..2f2728465f 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: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
 
 (** [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:TranspState.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:TranspState.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 -> TranspState.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:TranspState.t -> env ->
   evar_map -> constr -> constr -> evar_map option
 
 (** {6 Special-Purpose Reduction Functions } *)
@@ -302,13 +302,13 @@ 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 head_unfold_under_prod : TranspState.t -> 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 ->
+  TranspState.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..988d1c7579 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) when is_transparent_constant TranspState.full const ->
           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..c6a58fc1e9 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 -> TranspState.t) Hook.t
+val classes_transparent_state : unit -> TranspState.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..6e5295a912 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 TranspState.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 : TranspState.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 : TranspState.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 : TranspState.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 = TranspState.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 = TranspState.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 = TranspState.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 = TranspState.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 = TranspState.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 = TranspState.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 = TranspState.empty;
   check_applied_meta_types = false;
   use_pattern_unification = false;
   modulo_betaiota = false;
@@ -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 TranspState.full;
+              modulo_delta = TranspState.full;
 	      modulo_eta = true;
 	      modulo_betaiota = true }
 	    ty1 ty2
@@ -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 = TranspState.full in {
+  modulo_conv_on_closed_terms = Some TranspState.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 = TranspState.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 = TranspState.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 TranspState.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..b7b525c9fc 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 : TranspState.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 : TranspState.t;
+  modulo_delta_types : TranspState.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 : TranspState.t -> unify_flags
 
 val elim_flags : unit -> unify_flags
 val elim_no_delta_flags : unit -> unify_flags