Rename TranspState into TransparentState.

12 files changed, 57 insertions, 57 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index a23a085db5..81e487b77d 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 = TranspState.full;
+  modulo_delta_types = TransparentState.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 = TranspState.empty };
+  subterm_unify_flags = { flags with modulo_delta = TransparentState.empty };
   allow_K_in_toplevel_higher_order_unification = false;
   resolve_evars = true
 }
 
 let auto_unif_flags =
-  auto_unif_flags_of TranspState.full TranspState.empty
+  auto_unif_flags_of TransparentState.full TransparentState.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 TranspState.full st
+  auto_unif_flags_of TransparentState.full st
 
 let hintmap_of sigma secvars hdc concl =
   match hdc with
@@ -363,7 +363,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 	    let l =
 	      match hdc with None -> Hint_db.map_none ~secvars db
 	      | Some hdc ->
-                  if TranspState.is_empty st
+                  if TransparentState.is_empty st
 		  then Hint_db.map_auto sigma ~secvars hdc concl db
 		  else Hint_db.map_existential sigma ~secvars hdc concl db
 	    in auto_flags_of_state st, l
diff --git a/tactics/auto.mli b/tactics/auto.mli
index c7acbd4bfb..72d2292ffb 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 : TranspState.t -> Unification.unify_flags
+val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
 
 val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
   Proofview.Goal.t -> clausenv * constr
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 04fe6a9fa7..2f2bd8d2bc 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -72,10 +72,10 @@ let constr_pat_discr t =
 let constr_val_discr_st sigma ts t =
   let c, l = decomp sigma t in
     match EConstr.kind sigma c with
-    | Const (c,u) -> if TranspState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l)
+    | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l)
     | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
     | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
-    | Var id when not (TranspState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l)
+    | Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Label(ProdLabel, [d; c])
     | Lambda (n, d, c) -> 
       if List.is_empty l then 
@@ -89,11 +89,11 @@ let constr_pat_discr_st ts t =
   match decomp_pat t with
   | PRef ((IndRef _) as ref), args
   | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
-  | PRef ((VarRef v) as ref), args when not (TranspState.is_transparent_variable ts v) ->
+  | PRef ((VarRef v) as ref), args when not (TransparentState.is_transparent_variable ts v) ->
       Some(GRLabel ref,args)
-  | PVar v, args when not (TranspState.is_transparent_variable ts v) ->
+  | PVar v, args when not (TransparentState.is_transparent_variable ts v) ->
       Some(GRLabel (VarRef v),args)
-  | PRef ((ConstRef c) as ref), args when not (TranspState.is_transparent_constant ts c) ->
+  | PRef ((ConstRef c) as ref), args when not (TransparentState.is_transparent_constant ts c) ->
       Some (GRLabel ref, args)
   | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
   | PLambda (_, d, c), [] -> Some (LambdaLabel, [d ; c])
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 6af5012def..cc31fb0599 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -18,7 +18,7 @@ open Pattern
 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 [TranspState.t]
+number of nodes of the patterns matching the term. The [TransparentState.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]. *)
@@ -30,10 +30,10 @@ sig
 
   val empty : t
 
-  val add : TranspState.t option -> t -> (constr_pattern * Z.t) -> t
-  val rmv : TranspState.t option -> t -> (constr_pattern * Z.t) -> t
+  val add : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t
+  val rmv : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t
 
-  val lookup : Evd.evar_map -> TranspState.t option -> t -> EConstr.constr -> Z.t list
+  val lookup : Evd.evar_map -> TransparentState.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 f27e5e281a..1bb33f2a23 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 TranspState.full true)
+       Hint_db.empty TransparentState.full true)
 
-  let make_autogoal_hints only_classes ?(st=TranspState.full) g =
+  let make_autogoal_hints only_classes ?(st=TransparentState.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=TranspState.full) only_classes dep cut i g =
+  let make_autogoal ?(st=TransparentState.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=TranspState.full) only_classes dep hints depth =
+  let search_tac ?(st=TransparentState.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=TranspState.full) ?(unique=false)
+  let eauto_tac ?(st=TransparentState.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=TranspState.full)
+let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.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 9e2b0d26b5..46dff34f89 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:TranspState.t -> ?strategy:search_strategy ->
+val typeclasses_eauto : ?only_classes:bool -> ?st:TransparentState.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:TranspState.t ->
+    ?st:TransparentState.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 c18b7bb214..9a6bdab7b9 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 TranspState.full
+let eauto_unif_flags = auto_flags_of_state TransparentState.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:TranspState.full true s.local_lemmas)
+                       else make_local_hint_db (pf_env gls) (project gls) ~ts:TransparentState.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:TranspState.full true lems in
+  let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:TransparentState.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 8377cd5c75..969f539d1f 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 = TranspState.empty;
-  modulo_delta_types = TranspState.empty;
+  modulo_delta = TransparentState.empty;
+  modulo_delta_types = TransparentState.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 TranspState.full;
+  modulo_conv_on_closed_terms = Some TransparentState.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 = TranspState.empty;
-  modulo_delta_types = TranspState.full;
+  modulo_delta = TransparentState.empty;
+  modulo_delta_types = TransparentState.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 TranspState.full;
+  modulo_conv_on_closed_terms = Some TransparentState.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 = TranspState.full;
-  modulo_delta_types = TranspState.full;
+  modulo_delta = TransparentState.full;
+  modulo_delta_types = TransparentState.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 287e289c2f..6aa021543d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -291,8 +291,8 @@ let lookup_tacs sigma concl st se =
 module Constr_map = Map.Make(GlobRef.Ordered)
 
 let is_transparent_gr ts = function
-  | VarRef id -> TranspState.is_transparent_variable ts id
-  | ConstRef cst -> TranspState.is_transparent_constant ts cst
+  | VarRef id -> TransparentState.is_transparent_variable ts id
+  | ConstRef cst -> TransparentState.is_transparent_constant ts cst
   | IndRef _ | ConstructRef _ -> false
 
 let strip_params env sigma c = 
@@ -497,7 +497,7 @@ type hint_db_name = string
 module Hint_db :
 sig
 type t
-val empty : ?name:hint_db_name -> TranspState.t -> bool -> t
+val empty : ?name:hint_db_name -> TransparentState.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 -> TranspState.t
-val set_transparent_state : t -> TranspState.t -> t
+val transparent_state : t -> TransparentState.t
+val set_transparent_state : t -> TransparentState.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 : TranspState.t;
+    hintdb_state : TransparentState.t;
     hintdb_cut : hints_path;
     hintdb_unfolds : Id.Set.t * Cset.t;
     hintdb_max_id : int;
@@ -664,7 +664,7 @@ struct
       match v.code.obj with
       | Unfold_nth egr ->
           let addunf ts (ids, csts) =
-            let open TranspState in
+            let open TransparentState in
 	    match egr with
             | EvalVarRef id ->
               { ts with tr_var = Id.Pred.add id ts.tr_var }, (Id.Set.add id ids, csts)
@@ -743,8 +743,8 @@ let typeclasses_db = "typeclass_instances"
 let rewrite_db = "rewrite"
 
 let auto_init_db =
-  Hintdbmap.add typeclasses_db (Hint_db.empty TranspState.full true)
-    (Hintdbmap.add rewrite_db (Hint_db.empty TranspState.cst_full true)
+  Hintdbmap.add typeclasses_db (Hint_db.empty TransparentState.full true)
+    (Hintdbmap.add rewrite_db (Hint_db.empty TransparentState.cst_full true)
        Hintdbmap.empty)
 
 let searchtable = Summary.ref ~name:"searchtable" auto_init_db
@@ -980,7 +980,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 TranspState.empty false
+  with Not_found -> Hint_db.empty ~name:dbname TransparentState.empty false
 
 let add_hint dbname hintlist =
   let check (_, h) =
@@ -998,7 +998,7 @@ let add_hint dbname hintlist =
     searchtable_add (dbname,db')
 
 let add_transparency dbname target b =
-  let open TranspState in
+  let open TransparentState in
   let db = get_db dbname in
   let st = Hint_db.transparent_state db in
   let st' =
@@ -1019,7 +1019,7 @@ let remove_hint dbname grs =
     searchtable_add (dbname, db')
 
 type hint_action =
-  | CreateDB of bool * TranspState.t
+  | CreateDB of bool * TransparentState.t
   | AddTransparency of evaluable_global_reference hints_transparency_target * bool
   | AddHints of hint_entry list
   | RemoveHints of GlobRef.t list
@@ -1547,7 +1547,7 @@ let pr_hint_db_env env sigma db =
     in
     Hint_db.fold fold db (mt ())
   in
-  let { TranspState.tr_var = ids; tr_cst = csts } = Hint_db.transparent_state db in
+  let { TransparentState.tr_var = ids; tr_cst = csts } = Hint_db.transparent_state db in
   hov 0
     ((if Hint_db.use_dn db then str"Discriminated database"
       else str"Non-discriminated database")) ++ fnl () ++
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 43cfb6a059..dd2c63d351 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 -> TranspState.t -> bool -> t
+    val empty : ?name:hint_db_name -> TransparentState.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 -> TranspState.t
-    val set_transparent_state : t -> TranspState.t -> t
+    val transparent_state : t -> TransparentState.t
+    val set_transparent_state : t -> TransparentState.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 -> TranspState.t -> bool -> unit
+val create_hint_db : bool -> hint_db_name -> TransparentState.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:TranspState.t -> bool -> delayed_open_constr list -> hint_db
+val make_local_hint_db : env -> evar_map -> ?ts:TransparentState.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 2601b5fd84..349cfce205 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 TranspState.full
+      else TransparentState.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 TranspState.full
+      else TransparentState.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=TranspState.full) x y =
+let unify ?(state=TransparentState.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=TranspState.full) 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 = TranspState.empty } }
+      subterm_unify_flags = { core_flags with modulo_delta = TransparentState.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 1db65fc1aa..4e91a9a728 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:TranspState.t -> constr -> constr -> unit Proofview.tactic
+val unify           : ?state:TransparentState.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