aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.md4
-rw-r--r--kernel/cClosure.ml31
-rw-r--r--kernel/cClosure.mli8
-rw-r--r--kernel/conv_oracle.ml3
-rw-r--r--kernel/transpState.ml37
-rw-r--r--kernel/transpState.mli10
-rw-r--r--plugins/firstorder/ground.ml12
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--pretyping/evarconv.ml7
-rw-r--r--pretyping/reductionops.ml23
-rw-r--r--pretyping/reductionops.mli1
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/unification.ml24
-rw-r--r--printing/printer.ml6
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--tactics/auto.ml4
-rw-r--r--tactics/btermdn.ml14
-rw-r--r--tactics/hints.ml34
-rw-r--r--vernac/assumptions.ml3
19 files changed, 117 insertions, 110 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index b1fdfafd3a..9c5785758d 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -19,6 +19,10 @@ Names
Constant.make3 has been removed, use Constant.make2
Constant.repr3 has been removed, use Constant.repr2
+- `Names.transparent_state` has been moved to its own module `TranspState`.
+ This module gathers utility functions that used to be defined in several
+ places.
+
Coqlib:
- Most functions from the `Coqlib` module have been deprecated in favor of
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
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 9d41ee0695..26710a64d0 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -24,14 +24,6 @@ val with_stats: 'a Lazy.t -> 'a
Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
a LetIn expression is Letin reduction *)
-
-
-val all_opaque : TranspState.t
-val all_transparent : TranspState.t
-
-val is_transparent_variable : TranspState.t -> variable -> bool
-val is_transparent_constant : TranspState.t -> Constant.t -> bool
-
(** Sets of reduction kinds. *)
module type RedFlagsSig = sig
type reds
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index ac78064235..c66beb49b8 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -81,7 +81,8 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu =
let accu = Id.Map.fold fvar var_opacity accu in
Cmap.fold fcst cst_opacity accu
-let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate)
+let get_transp_state { var_trstate; cst_trstate; _ } =
+ { TranspState.tr_var = var_trstate; tr_cst = cst_trstate }
let dep_order l2r k1 k2 = match k1, k2 with
| RelKey _, RelKey _ -> l2r
diff --git a/kernel/transpState.ml b/kernel/transpState.ml
index 9acb7244f7..9661dace6a 100644
--- a/kernel/transpState.ml
+++ b/kernel/transpState.ml
@@ -10,9 +10,36 @@
open Names
-type t = Id.Pred.t * Cpred.t
+type t = {
+ tr_var : Id.Pred.t;
+ tr_cst : Cpred.t;
+}
-let empty = (Id.Pred.empty, Cpred.empty)
-let full = (Id.Pred.full, Cpred.full)
-let var_full = (Id.Pred.full, Cpred.empty)
-let cst_full = (Id.Pred.empty, Cpred.full)
+let empty = {
+ tr_var = Id.Pred.empty;
+ tr_cst = Cpred.empty;
+}
+
+let full = {
+ tr_var = Id.Pred.full;
+ tr_cst = Cpred.full;
+}
+
+let var_full = {
+ tr_var = Id.Pred.full;
+ tr_cst = Cpred.empty;
+}
+
+let cst_full = {
+ tr_var = Id.Pred.empty;
+ tr_cst = Cpred.full;
+}
+
+let is_empty ts =
+ Id.Pred.is_empty ts.tr_var && Cpred.is_empty ts.tr_cst
+
+let is_transparent_variable ts id =
+ Id.Pred.mem id ts.tr_var
+
+let is_transparent_constant ts cst =
+ Cpred.mem cst ts.tr_cst
diff --git a/kernel/transpState.mli b/kernel/transpState.mli
index a8d301549b..f2999c6869 100644
--- a/kernel/transpState.mli
+++ b/kernel/transpState.mli
@@ -11,7 +11,10 @@
open Names
(** Sets of names *)
-type t = Id.Pred.t * Cpred.t
+type t = {
+ tr_var : Id.Pred.t;
+ tr_cst : Cpred.t;
+}
val empty : t
(** Everything opaque *)
@@ -24,3 +27,8 @@ val var_full : t
val cst_full : t
(** All constant transparent *)
+
+val is_empty : t -> bool
+
+val is_transparent_variable : t -> Id.t -> bool
+val is_transparent_constant : t -> Constant.t -> bool
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 516b04ea21..820dd97043 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -18,16 +18,16 @@ open Tacticals.New
open Globnames
let update_flags ()=
- let f acc coe =
- match coe.Classops.coe_value with
- | ConstRef c -> Names.Cpred.add c acc
- | _ -> acc
+ let open TranspState in
+ let f accu coe = match coe.Classops.coe_value with
+ | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
+ | _ -> accu
in
- let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in
+ let flags = List.fold_left f TranspState.full (Classops.coercions ()) in
red_flags:=
CClosure.RedFlags.red_add_transparent
CClosure.betaiotazeta
- (Names.Id.Pred.full,Names.Cpred.complement pred)
+ flags
let ground_tac solver startseq =
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1f31a617be..d66184227e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -528,7 +528,7 @@ let decompose_applied_relation env sigma (c,l) =
let rewrite_db = "rewrite"
-let conv_transparent_state = (Id.Pred.empty, Cpred.full)
+let conv_transparent_state = TranspState.cst_full
let rewrite_transparent_state () =
Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 68b53787f9..0c9ad5d094 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -16,7 +16,6 @@ open Termops
open Environ
open EConstr
open Vars
-open CClosure
open Reduction
open Reductionops
open Recordops
@@ -74,14 +73,14 @@ let coq_unit_judge =
let unfold_projection env evd ts p c =
let cst = Projection.constant p in
- if is_transparent_constant ts cst then
+ if TranspState.is_transparent_constant ts cst then
Some (mkProj (Projection.unfold p, c))
else None
let eval_flexible_term ts env evd c =
match EConstr.kind evd c with
| Const (c, u) ->
- if is_transparent_constant ts c
+ if TranspState.is_transparent_constant ts c
then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u))
else None
| Rel n ->
@@ -91,7 +90,7 @@ let eval_flexible_term ts env evd c =
with Not_found -> None)
| Var id ->
(try
- if is_transparent_variable ts id then
+ if TranspState.is_transparent_variable ts id then
env |> lookup_named id |> NamedDecl.get_value
else None
with Not_found -> None)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 18b0bab892..4fbbf20c1f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -675,10 +675,6 @@ let apply_subst recfun env sigma refold cst_l t stack =
let stacklam recfun env sigma t stack =
apply_subst (fun _ _ s -> recfun s) env sigma false Cst_stack.empty t stack
-let beta_app sigma (c,l) =
- let zip s = Stack.zip sigma s in
- stacklam zip [] sigma c (Stack.append_app l Stack.empty)
-
let beta_applist sigma (c,l) =
let zip s = Stack.zip sigma s in
stacklam zip [] sigma c (Stack.append_app_list l Stack.empty)
@@ -1681,25 +1677,6 @@ let meta_reducible_instance evd b =
if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
else irec b.rebus
-
-let head_unfold_under_prod ts env sigma c =
- let unfold (cst,u) =
- let cstu = (cst, EInstance.kind sigma u) in
- if Cpred.mem cst (snd ts) then
- match constant_opt_value_in env cstu with
- | Some c -> EConstr.of_constr c
- | None -> mkConstU (cst, u)
- else mkConstU (cst, u) in
- let rec aux c =
- match EConstr.kind sigma c with
- | Prod (n,t,c) -> mkProd (n,aux t, aux c)
- | _ ->
- let (h,l) = decompose_app_vect sigma c in
- match EConstr.kind sigma h with
- | Const cst -> beta_app sigma (unfold cst, l)
- | _ -> c in
- aux c
-
let betazetaevar_applist sigma n c l =
let rec stacklam n env t stack =
if Int.equal n 0 then applist (substl env t, stack) else
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 2f2728465f..749e23bde2 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -302,7 +302,6 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TranspState.t ->
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 : TranspState.t -> reduction_function
val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
(** {6 Heuristic for Conversion with Evar } *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 988d1c7579..d9df8c8cf8 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 TranspState.full const ->
+ | Const (const, u) ->
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/unification.ml b/pretyping/unification.ml
index 6e5295a912..99b8d8e92a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -504,16 +504,16 @@ let key_of env sigma b flags f =
if subterm_restriction b flags then None else
match EConstr.kind sigma f with
| Const (cst, u) when is_transparent env (ConstKey cst) &&
- (Cpred.mem cst (snd flags.modulo_delta)
+ (TranspState.is_transparent_constant flags.modulo_delta cst
|| Recordops.is_primitive_projection cst) ->
let u = EInstance.kind sigma u in
Some (IsKey (ConstKey (cst, u)))
| Var id when is_transparent env (VarKey id) &&
- Id.Pred.mem id (fst flags.modulo_delta) ->
+ TranspState.is_transparent_variable flags.modulo_delta id ->
Some (IsKey (VarKey id))
| Proj (p, c) when Projection.unfolded p
|| (is_transparent env (ConstKey (Projection.constant p)) &&
- (Cpred.mem (Projection.constant p) (snd flags.modulo_delta))) ->
+ (TranspState.is_transparent_constant flags.modulo_delta (Projection.constant p))) ->
Some (IsProj (p, c))
| _ -> None
@@ -550,7 +550,7 @@ let oracle_order env cf1 cf2 =
let is_rigid_head sigma flags t =
match EConstr.kind sigma t with
- | Const (cst,u) -> not (Cpred.mem cst (snd flags.modulo_delta))
+ | Const (cst,u) -> not (TranspState.is_transparent_constant flags.modulo_delta cst)
| Ind (i,u) -> true
| Construct _ -> true
| Fix _ | CoFix _ -> true
@@ -633,11 +633,11 @@ let rec is_neutral env sigma ts t =
| Const (c, u) ->
not (Environ.evaluable_constant c env) ||
not (is_transparent env (ConstKey c)) ||
- not (Cpred.mem c (snd ts))
+ not (TranspState.is_transparent_constant ts c)
| Var id ->
not (Environ.evaluable_named id env) ||
not (is_transparent env (VarKey id)) ||
- not (Id.Pred.mem id (fst ts))
+ not (TranspState.is_transparent_variable ts id)
| Rel n -> true
| Evar _ | Meta _ -> true
| Case (_, p, c, cl) -> is_neutral env sigma ts c
@@ -1120,10 +1120,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
| Some sigma -> ans
| None ->
if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
- | Some (cv_id, cv_k), (dl_id, dl_k) ->
- Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
- | None,(dl_id, dl_k) ->
- Id.Pred.is_empty dl_id && Cpred.is_empty dl_k)
+ | Some cv, dl ->
+ let open TranspState in
+ Id.Pred.subset dl.tr_var cv.tr_var && Cpred.subset dl.tr_cst cv.tr_cst
+ | None, dl -> TranspState.is_empty dl)
then error_cannot_unify env sigma (m, n) else None
in
let a = match res with
@@ -1263,8 +1263,8 @@ let applyHead env evd n c =
let is_mimick_head sigma ts f =
match EConstr.kind sigma f with
- | Const (c,u) -> not (CClosure.is_transparent_constant ts c)
- | Var id -> not (CClosure.is_transparent_variable ts id)
+ | Const (c,u) -> not (TranspState.is_transparent_constant ts c)
+ | Var id -> not (TranspState.is_transparent_variable ts id)
| (Rel _|Construct _|Ind _) -> true
| _ -> false
diff --git a/printing/printer.ml b/printing/printer.ml
index da364c8b9e..b7c53c5513 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -445,9 +445,9 @@ let pr_predicate pr_elt (b, elts) =
let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p)
-let pr_transparent_state (ids, csts) =
- hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
- str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
+let pr_transparent_state ts =
+ hv 0 (str"VARIABLES: " ++ pr_idpred ts.TranspState.tr_var ++ fnl () ++
+ str"CONSTANTS: " ++ pr_cpred ts.TranspState.tr_cst ++ fnl ())
(* display complete goal
og_s has goal+sigma on the previous proof step for diffs
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 56ce744bc1..1aaf762e31 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -160,7 +160,7 @@ let make_flag env f =
(fun v red -> red_sub red (make_flag_constant v))
f.rConst red
else (* Only rConst *)
- let red = red_add_transparent (red_add red fDELTA) all_opaque in
+ let red = red_add_transparent (red_add red fDELTA) TranspState.empty in
List.fold_right
(fun v red -> red_add red (make_flag_constant v))
f.rConst red
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 07b9bac2c7..a23a085db5 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -358,12 +358,12 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
let flags = flags_of_state (Hint_db.transparent_state db) in
List.map (fun x -> (Some flags, x)) (f db)
else
- let (ids, csts as st) = Hint_db.transparent_state db in
+ let st = Hint_db.transparent_state db in
let flags, l =
let l =
match hdc with None -> Hint_db.map_none ~secvars db
| Some hdc ->
- if (Id.Pred.is_empty ids && Cpred.is_empty csts)
+ if TranspState.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/btermdn.ml b/tactics/btermdn.ml
index bfee0422e7..04fe6a9fa7 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -69,13 +69,13 @@ let constr_pat_discr t =
| PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args)
| _ -> None
-let constr_val_discr_st sigma (idpred,cpred) 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 Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l)
+ | Const (c,u) -> if TranspState.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 (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l)
+ | Var id when not (TranspState.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
@@ -85,15 +85,15 @@ let constr_val_discr_st sigma (idpred,cpred) t =
| Evar _ -> Everything
| _ -> Nothing
-let constr_pat_discr_st (idpred,cpred) t =
+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 (Id.Pred.mem v idpred) ->
+ | PRef ((VarRef v) as ref), args when not (TranspState.is_transparent_variable ts v) ->
Some(GRLabel ref,args)
- | PVar v, args when not (Id.Pred.mem v idpred) ->
+ | PVar v, args when not (TranspState.is_transparent_variable ts v) ->
Some(GRLabel (VarRef v),args)
- | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) ->
+ | PRef ((ConstRef c) as ref), args when not (TranspState.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/hints.ml b/tactics/hints.ml
index 5f0d3a2503..287e289c2f 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 -> TranspState.is_transparent_variable ts id
+ | ConstRef cst -> TranspState.is_transparent_constant ts cst
| IndRef _ | ConstructRef _ -> false
let strip_params env sigma c =
@@ -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 TranspState 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
@@ -995,18 +998,19 @@ let add_hint dbname hintlist =
searchtable_add (dbname,db')
let add_transparency dbname target b =
+ let open TranspState 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 =
@@ -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 { TranspState.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/vernac/assumptions.ml b/vernac/assumptions.ml
index 6beac2032d..b51b6cedfb 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -294,7 +294,6 @@ let traverse current t =
let type_of_constant cb = cb.Declarations.const_type
let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
- let (idts, knst) = st in
(** Only keep the transitive dependencies *)
let (_, graph, ax2ty) = traverse (label_of gr) t in
let fold obj _ accu = match obj with
@@ -316,7 +315,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let t = type_of_constant cb in
let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Constant kn,l)) t accu
- else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
+ else if add_opaque && (Declareops.is_opaque cb || not (TranspState.is_transparent_constant st kn)) then
let t = type_of_constant cb in
ContextObjectMap.add (Opaque kn) t accu
else if add_transparent then
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-06 03:10:22 +0000