diff options
Diffstat (limited to 'plugins/subtac/subtac_obligations.ml')
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index a54b3a86f..a8f5815bc 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -77,7 +77,7 @@ let _ = declare_bool_option { optsync = true; optname = "transparency of Program obligations"; - optkey = (SecondaryTable ("Transparent","Obligations")); + optkey = ["Transparent";"Obligations"]; optread = get_proofs_transparency; optwrite = set_proofs_transparency; } |