Move transparent_state to its own module.

11 files changed, 46 insertions, 47 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 65b2615b6b..07b9bac2c7 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 = TranspState.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 = TranspState.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 TranspState.full TranspState.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 TranspState.full st
 
 let hintmap_of sigma secvars hdc concl =
   match hdc with
diff --git a/tactics/auto.mli b/tactics/auto.mli
index a835c1ed95..c7acbd4bfb 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 : TranspState.t -> Unification.unify_flags
 
 val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
   Proofview.Goal.t -> clausenv * constr
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 861c9b6250..6af5012def 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 [TranspState.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 : TranspState.t option -> t -> (constr_pattern * Z.t) -> t
+  val rmv : TranspState.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 -> TranspState.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..f27e5e281a 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 TranspState.full true)
 
-  let make_autogoal_hints only_classes ?(st=full_transparent_state) g =
+  let make_autogoal_hints only_classes ?(st=TranspState.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=TranspState.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=TranspState.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=TranspState.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=TranspState.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..9e2b0d26b5 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:TranspState.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:TranspState.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..c18b7bb214 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 TranspState.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:TranspState.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:TranspState.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..8377cd5c75 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 = TranspState.empty;
+  modulo_delta_types = TranspState.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 TranspState.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 = TranspState.empty;
+  modulo_delta_types = TranspState.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 TranspState.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 = TranspState.full;
+  modulo_delta_types = TranspState.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 2f2d32e887..5f0d3a2503 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -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 -> TranspState.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 -> TranspState.t
+val set_transparent_state : t -> TranspState.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 : TranspState.t;
     hintdb_cut : hints_path;
     hintdb_unfolds : Id.Set.t * Cset.t;
     hintdb_max_id : int;
@@ -740,8 +740,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 TranspState.full true)
+    (Hintdbmap.add rewrite_db (Hint_db.empty TranspState.cst_full true)
        Hintdbmap.empty)
 
 let searchtable = Summary.ref ~name:"searchtable" auto_init_db
@@ -977,7 +977,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 TranspState.empty false
 
 let add_hint dbname hintlist =
   let check (_, h) =
@@ -1015,7 +1015,7 @@ let remove_hint dbname grs =
     searchtable_add (dbname, db')
 
 type hint_action =
-  | CreateDB of bool * transparent_state
+  | CreateDB of bool * TranspState.t
   | AddTransparency of evaluable_global_reference hints_transparency_target * bool
   | AddHints of hint_entry list
   | RemoveHints of GlobRef.t list
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 6db8feccd0..43cfb6a059 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 -> TranspState.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 -> TranspState.t
+    val set_transparent_state : t -> TranspState.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 -> TranspState.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:TranspState.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..2601b5fd84 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 TranspState.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 TranspState.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=TranspState.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 = TranspState.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..1db65fc1aa 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:TranspState.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