diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrprinters.ml | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 2 |
5 files changed, 6 insertions, 11 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index a5f23c4d9e..895f491510 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -33,8 +33,7 @@ open Tacmach let ssroldreworder = Summary.ref ~name:"SSR:oldreworder" false let () = Goptions.(declare_bool_option - { optname = "ssreflect 1.3 compatibility flag"; - optkey = ["SsrOldRewriteGoalsOrder"]; + { optkey = ["SsrOldRewriteGoalsOrder"]; optread = (fun _ -> !ssroldreworder); optdepr = false; optwrite = (fun b -> ssroldreworder := b) }) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index a97aba9166..a6b9a43778 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -69,8 +69,7 @@ let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false let () = Goptions.(declare_bool_option - { optname = "have type classes"; - optkey = ["SsrHave";"NoTCResolution"]; + { optkey = ["SsrHave";"NoTCResolution"]; optread = (fun _ -> !ssrhaveNOtcresolution); optdepr = false; optwrite = (fun b -> ssrhaveNOtcresolution := b); diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 22325f3fc3..21b832a326 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1662,8 +1662,7 @@ let ssr_reserved_ids = Summary.ref ~name:"SSR:idents" true let () = Goptions.(declare_bool_option - { optname = "ssreflect identifiers"; - optkey = ["SsrIdents"]; + { optkey = ["SsrIdents"]; optdepr = false; optread = (fun _ -> !ssr_reserved_ids); optwrite = (fun b -> ssr_reserved_ids := b) @@ -2395,8 +2394,7 @@ let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true let () = Goptions.(declare_bool_option - { optname = "ssreflect rewrite"; - optkey = ["SsrRewrite"]; + { optkey = ["SsrRewrite"]; optread = (fun _ -> !ssr_rw_syntax); optdepr = false; optwrite = (fun b -> ssr_rw_syntax := b) }) diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index f0aed1a934..22250202b5 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -134,8 +134,7 @@ let ppdebug_ref = ref (fun _ -> ()) let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) let () = Goptions.(declare_bool_option - { optname = "ssreflect debugging"; - optkey = ["Debug";"Ssreflect"]; + { optkey = ["Debug";"Ssreflect"]; optdepr = false; optread = (fun _ -> !ppdebug_ref == ssr_pp); optwrite = (fun b -> diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index d8dbf2f3dc..b212e7046a 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -151,7 +151,7 @@ let declare_one_prenex_implicit locality f = with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> - Impargs.MaximallyImplicit :: loop args' + MaxImplicit :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> errorstrm (str "Expected prenex implicits for " ++ pr_qualid f) | _ -> [] in |