Merge pull request MetaCoq#968 from SkySkimmer/depr-versions

Adapt to coq/coq#17664 (goptions use Deprecation.t option instead of bool)
SkySkimmer · Jun 6, 2023 · b34d3f3 · b34d3f3
2 parents 54455b9 + d5c0dcb
commit b34d3f3
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git a/template-coq/src/g_template_coq.mlg b/template-coq/src/g_template_coq.mlg
@@ -29,7 +29,7 @@ open Redexpr
 let _ =
   let open Goptions in
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = None;
       optstage = Interp;
       optkey   = ["MetaCoq"; "Strict"; "Unquote"; "Universe"; "Mode"];
       optread  = (fun () -> !Denoter.strict_unquote_universe_mode);

diff --git a/template-coq/src/tm_util.ml b/template-coq/src/tm_util.ml
@@ -24,7 +24,7 @@ end = struct
       | _  -> assert false
       end
     | None ->
-      declare_int_option_and_ref ~stage:Interp ~depr:false ~key ~value:0
+      match declare_int_option_and_ref ~key ~value:0 () with { get } -> get
 
   let set_template_monad_verbose =
     let open Goptions in
@@ -47,7 +47,7 @@ end = struct
     | Some get -> ()
     | None ->
       declare_bool_option
-        { optdepr  = false;
+        { optdepr  = None;
           optstage = Interp;
           optkey   = key;
           optread  = get_template_monad_debug;
@@ -68,7 +68,8 @@ let timing_opt =
       | BoolValue b -> b
       | _ -> assert false
       end
-  | None -> declare_bool_option_and_ref ~stage:Interp ~depr:false ~key ~value:false
+  | None ->
+    match declare_bool_option_and_ref ~key ~value:false () with { get } -> get
 
 let time prefix f x =
   if timing_opt () then
@@ -88,7 +89,8 @@ let debug_opt =
       | BoolValue b -> b
       | _ -> assert false
       end
-  | None -> declare_bool_option_and_ref ~stage:Interp ~depr:false ~key ~value:false
+  | None ->
+    match declare_bool_option_and_ref ~key ~value:false () with { get } -> get
 
 let debug (m : unit ->Pp.t) =
   if debug_opt () then