diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-15 17:47:27 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-15 17:47:27 +0100 |
| commit | 484d69c8e59823f0a1fb4f1b99b371c8bdecd880 (patch) | |
| tree | 46fc70a88ea96691c12e6424e5c05cc00c514574 /plugins | |
| parent | 5ae35a94dd3ec72d9ac91ba3b34674dd79a78263 (diff) | |
| parent | 539a62a79f75f9f5190b9bd8edfbb04b880a5f1f (diff) | |
Merge PR #6219: Document undocumented options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 938bec25b..b81010c7b 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -40,17 +40,17 @@ let _= in declare_int_option gdopt -let congruence_depth=ref 100 let _= + let congruence_depth=ref 100 in let gdopt= - { optdepr=false; + { optdepr=true; (* noop *) optname="Congruence Depth"; optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); optwrite= (function - None->congruence_depth:=0 + None->congruence_depth:=0 | Some i->congruence_depth:=(max i 0))} in declare_int_option gdopt diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index bd9633afb..6032ed2af 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -143,14 +143,14 @@ let newssrcongrtac arg ist gl = (** Coq rewrite compatibility flag *) -let ssr_strict_match = ref false let _ = - Goptions.declare_bool_option + let ssr_strict_match = ref false in + Goptions.declare_bool_option { Goptions.optname = "strict redex matching"; Goptions.optkey = ["Match"; "Strict"]; Goptions.optread = (fun () -> !ssr_strict_match); - Goptions.optdepr = false; + Goptions.optdepr = true; (* noop *) Goptions.optwrite = (fun b -> ssr_strict_match := b) } (** Rewrite rules *) |