aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/decl_proof_instr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/decl_proof_instr.ml')
-rw-r--r--tactics/decl_proof_instr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index e909a1f4f..515b184da 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -44,7 +44,7 @@ let _ =
declare_bool_option
{ optsync = true;
optname = "strict mode";
- optkey = (SecondaryTable ("Strict","Proofs"));
+ optkey = ["Strict";"Proofs"];
optread = get_strictness;
optwrite = set_strictness }