3 files changed, 23 insertions, 10 deletions
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index ca6ae150a7..15cf88f827 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -195,16 +195,29 @@ let is_interactive recsl =
 
 }
 
+(* For usability we temporarily switch off some flags during the call
+   to Function. However this is not satisfactory:
+
+ 1- Function should not warn "non-recursive" and call the Definition
+    mechanism instead of Fixpoint when needed
+
+ 2- Only for automatically generated names should
+    unused-pattern-matching-variable be ignored. *)
+
 VERNAC COMMAND EXTEND Function STATE CUSTOM
 | ["Function" ne_function_fix_definition_list_sep(recsl,"with")]
     => { classify_funind recsl }
     -> {
-         if is_interactive recsl then
-           Vernacextend.VtOpenProof (fun () ->
-             Gen_principle.do_generate_principle_interactive (List.map snd recsl))
-         else
-           Vernacextend.VtDefault (fun () ->
-             Gen_principle.do_generate_principle (List.map snd recsl)) }
+    let warn = "-unused-pattern-matching-variable,-matching-variable,-non-recursive" in
+    if is_interactive recsl then
+      Vernacextend.VtOpenProof (fun () ->
+          CWarnings.with_warn warn
+            Gen_principle.do_generate_principle_interactive (List.map snd recsl))
+    else
+      Vernacextend.VtDefault (fun () ->
+          CWarnings.with_warn warn
+            Gen_principle.do_generate_principle (List.map snd recsl))
+  }
 END
 
 {
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 74d5374193..ed608bb1df 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -28,7 +28,7 @@ open Q.Notations
 open Mutils
 
 let use_simplex =
-  Goptions.declare_bool_option_and_ref ~depr:false ~key:["Simplex"] ~value:true
+  Goptions.declare_bool_option_and_ref ~depr:true ~key:["Simplex"] ~value:true
 
 (* If set to some [file], arithmetic goals are dumped in [file].v *)
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 5e138fa3d1..91f7e27911 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -38,14 +38,14 @@ let max_depth = max_int
 
 (* Search limit for provers over Q R *)
 let lra_proof_depth =
-  declare_int_option_and_ref ~depr:false ~key:["Lra"; "Depth"] ~value:max_depth
+  declare_int_option_and_ref ~depr:true ~key:["Lra"; "Depth"] ~value:max_depth
 
 (* Search limit for provers over Z *)
 let lia_enum =
-  declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Enum"] ~value:true
+  declare_bool_option_and_ref ~depr:true ~key:["Lia"; "Enum"] ~value:true
 
 let lia_proof_depth =
-  declare_int_option_and_ref ~depr:false ~key:["Lia"; "Depth"] ~value:max_depth
+  declare_int_option_and_ref ~depr:true ~key:["Lia"; "Depth"] ~value:max_depth
 
 let get_lia_option () =
   (Certificate.use_simplex (), lia_enum (), lia_proof_depth ())