diff options
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 9c15d9d12..0f048f59a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -490,8 +490,8 @@ open Goptions let functional_induction_rewrite_dependent_proofs_sig = { optsync = false; - optname = "functional induction rewrite dependent"; - optkey = ["functional_induction_rewrite_dependent"]; + optname = "Functional Induction Rewrite Dependent"; + optkey = ["Functional";"Induction";"Rewrite";"Dependent"]; optread = (fun () -> !functional_induction_rewrite_dependent_proofs); optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b) } |