diff options
| author | Hugo Herbelin | 2016-09-03 11:45:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-09-03 11:46:15 +0200 |
| commit | 52b82dd42b93af6831df3bfea4822c6c8680a288 (patch) | |
| tree | 7a661eb53fb3e5eea29c0c85ab408c84caa05021 /plugins | |
| parent | af2df1ada04da94a41a400c637788db461a532d9 (diff) | |
Fixing what is probably a typo in Strict Proofs mode (#5062).
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index ba9fb728c1..0680139598 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -42,7 +42,7 @@ let _ = declare_bool_option { optsync = true; optdepr = false; - optname = "strict mode"; + optname = "strict proofs"; optkey = ["Strict";"Proofs"]; optread = get_strictness; optwrite = set_strictness } |