Proper record type and accessors for transparent states.

This is documented in dev/doc/changes.md.

1 files changed, 14 insertions, 17 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c8028f713a..625a9a7277 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -72,11 +72,8 @@ let with_stats c =
   end else
     Lazy.force c
 
-let all_opaque = (Id.Pred.empty, Cpred.empty)
-let all_transparent = (Id.Pred.full, Cpred.full)
-
-let is_transparent_variable (ids, _) id = Id.Pred.mem id ids
-let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
+let all_opaque = TranspState.empty
+let all_transparent = TranspState.full
 
 module type RedFlagsSig = sig
   type reds
@@ -106,6 +103,8 @@ module RedFlags = (struct
   (* [r_const=(false,cl)] means only those in [cl] *)
   (* [r_delta=true] just mean [r_const=(true,[])] *)
 
+  open TranspState
+
   type reds = {
     r_beta : bool;
     r_delta : bool;
@@ -143,30 +142,30 @@ module RedFlags = (struct
     | ETA -> { red with r_eta = true }
     | DELTA -> { red with r_delta = true; r_const = all_transparent }
     | CONST kn ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, Cpred.add kn l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_cst = Cpred.add kn r.tr_cst } }
     | MATCH -> { red with r_match = true }
     | FIX -> { red with r_fix = true }
     | COFIX -> { red with r_cofix = true }
     | ZETA -> { red with r_zeta = true }
     | VAR id ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = Id.Pred.add id l1, l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_var = Id.Pred.add id r.tr_var } }
 
   let red_sub red = function
     | BETA -> { red with r_beta = false }
     | ETA -> { red with r_eta = false }
     | DELTA -> { red with r_delta = false }
     | CONST kn ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, Cpred.remove kn l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_cst = Cpred.remove kn r.tr_cst } }
     | MATCH -> { red with r_match = false }
     | FIX -> { red with r_fix = false }
     | COFIX -> { red with r_cofix = false }
     | ZETA -> { red with r_zeta = false }
     | VAR id ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = Id.Pred.remove id l1, l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_var = Id.Pred.remove id r.tr_var } }
 
   let red_transparent red = red.r_const
 
@@ -179,12 +178,10 @@ module RedFlags = (struct
     | BETA -> incr_cnt red.r_beta beta
     | ETA -> incr_cnt red.r_eta eta
     | CONST kn ->
-	let (_,l) = red.r_const in
-	let c = Cpred.mem kn l in
+      let c = is_transparent_constant red.r_const kn in
 	incr_cnt c delta
     | VAR id -> (* En attendant d'avoir des kn pour les Var *)
-	let (l,_) = red.r_const in
-	let c = Id.Pred.mem id l in
+      let c = is_transparent_variable red.r_const id in
 	incr_cnt c delta
     | ZETA -> incr_cnt red.r_zeta zeta
     | MATCH -> incr_cnt red.r_match nb_match