Merge PR #7925: Clean transparent state

1 files changed, 27 insertions, 23 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 328d57c8a3..e64e08dbde 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -290,9 +290,9 @@ let lookup_tacs sigma concl st se =
 
 module Constr_map = Map.Make(GlobRef.Ordered)
 
-let is_transparent_gr (ids, csts) = function
-  | VarRef id -> Id.Pred.mem id ids
-  | ConstRef cst -> Cpred.mem cst csts
+let is_transparent_gr ts = function
+  | 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 -> transparent_state -> 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 -> transparent_state
-val set_transparent_state : t -> transparent_state -> 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 : Names.transparent_state;
+    hintdb_state : TransparentState.t;
     hintdb_cut : hints_path;
     hintdb_unfolds : Id.Set.t * Cset.t;
     hintdb_max_id : int;
@@ -663,10 +663,13 @@ struct
     let st',db,rebuild =
       match v.code.obj with
       | Unfold_nth egr ->
-	  let addunf (ids,csts) (ids',csts') =
+          let addunf ts (ids, csts) =
+            let open TransparentState in
 	    match egr with
-	    | EvalVarRef id -> (Id.Pred.add id ids, csts), (Id.Set.add id ids', csts')
-	    | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts')
+            | EvalVarRef id ->
+              { ts with tr_var = Id.Pred.add id ts.tr_var }, (Id.Set.add id ids, csts)
+            | EvalConstRef cst ->
+              { ts with tr_cst = Cpred.add cst ts.tr_cst }, (ids, Cset.add cst csts)
 	  in 
 	  let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
 	    state, { db with hintdb_unfolds = unfs }, true
@@ -740,8 +743,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 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
@@ -977,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 empty_transparent_state false
+  with Not_found -> Hint_db.empty ~name:dbname TransparentState.empty false
 
 let add_hint dbname hintlist =
   let check (_, h) =
@@ -995,18 +998,19 @@ let add_hint dbname hintlist =
     searchtable_add (dbname,db')
 
 let add_transparency dbname target b =
+  let open TransparentState in
   let db = get_db dbname in
-  let (ids, csts as st) = Hint_db.transparent_state db in
+  let st = Hint_db.transparent_state db in
   let st' =
     match target with
-    | HintsVariables -> (if b then Id.Pred.full else Id.Pred.empty), csts
-    | HintsConstants -> ids, if b then Cpred.full else Cpred.empty
+    | HintsVariables -> { st with tr_var = (if b then Id.Pred.full else Id.Pred.empty) }
+    | HintsConstants -> { st with tr_cst = (if b then Cpred.full else Cpred.empty) }
     | HintsReferences grs ->
-       List.fold_left (fun (ids, csts) gr ->
-       match gr with
-       | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts)
-       | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts)
-                      st grs
+      List.fold_left (fun st gr ->
+        match gr with
+        | EvalConstRef c -> { st with tr_cst = (if b then Cpred.add else Cpred.remove) c st.tr_cst }
+        | EvalVarRef v -> { st with tr_var = (if b then Id.Pred.add else Id.Pred.remove) v st.tr_var })
+        st grs
   in searchtable_add (dbname, Hint_db.set_transparent_state db st')
 
 let remove_hint dbname grs =
@@ -1015,7 +1019,7 @@ let remove_hint dbname grs =
     searchtable_add (dbname, db')
 
 type hint_action =
-  | CreateDB of bool * transparent_state
+  | CreateDB of bool * TransparentState.t
   | AddTransparency of evaluable_global_reference hints_transparency_target * bool
   | AddHints of hint_entry list
   | RemoveHints of GlobRef.t list
@@ -1543,7 +1547,7 @@ let pr_hint_db_env env sigma db =
     in
     Hint_db.fold fold db (mt ())
   in
-  let (ids, 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 () ++