diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/ground.ml | 12 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
2 files changed, 7 insertions, 7 deletions
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) |