diff options
| author | Pierre-Marie Pédrot | 2018-06-22 21:06:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:29:55 +0100 |
| commit | ad5aea737ecc639c31dda84322b3550a4d380b47 (patch) | |
| tree | c068b7493867b8fe0bab81e285bbc09adda1f7aa /plugins/ltac | |
| parent | 96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 (diff) | |
Proper record type and accessors for transparent states.
This is documented in dev/doc/changes.md.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |