4 files changed, 58 insertions, 18 deletions
diff --git a/plugins/micromega/Fourier.v b/plugins/micromega/Fourier.v
new file mode 100644
index 0000000000..0153de1dab
--- /dev/null
+++ b/plugins/micromega/Fourier.v
@@ -0,0 +1,5 @@
+Require Import Lra.
+Require Export Fourier_util.
+
+#[deprecated(since = "8.9.0", note = "Use lra instead.")]
+Ltac fourier := lra.
diff --git a/plugins/micromega/Fourier_util.v b/plugins/micromega/Fourier_util.v
new file mode 100644
index 0000000000..b62153dee4
--- /dev/null
+++ b/plugins/micromega/Fourier_util.v
@@ -0,0 +1,31 @@
+Require Export Rbase.
+Require Import Lra.
+
+Open Scope R_scope.
+
+Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.
+intros x y H H0; try assumption.
+replace 0 with (x * 0).
+apply Rmult_lt_compat_l; auto with real.
+ring.
+Qed.
+
+Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x.
+intros x H; try assumption.
+rewrite Rplus_comm.
+apply Rle_lt_0_plus_1.
+red; auto with real.
+Qed.
+
+Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x.
+  intros; lra.
+Qed.
+
+Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.
+intros x y H H0; try assumption.
+case H; intros.
+red; left.
+apply Rlt_mult_inv_pos; auto with real.
+rewrite <- H1.
+red; right; ring.
+Qed.
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.mlg
index 81140a46a9..21f0414e9c 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.mlg
@@ -16,70 +16,74 @@
 (*                                                                      *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
 open Stdarg
 open Tacarg
 
+}
+
 DECLARE PLUGIN "micromega_plugin"
 
 TACTIC EXTEND RED
-| [ "myred"  ] -> [ Tactics.red_in_concl ]
+| [ "myred"  ] -> { Tactics.red_in_concl }
 END
 
 
 
 TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) tactic(t) ] -> [  (Coq_micromega.psatz_Z i
+| [ "psatz_Z" int_or_var(i) tactic(t) ] -> {  (Coq_micromega.psatz_Z i
                                                (Tacinterp.tactic_of_value ist t))
-                                               ]
-| [ "psatz_Z" tactic(t)] -> [  (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) ]
+                                               }
+| [ "psatz_Z" tactic(t)] -> {  (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) }
 END
 
 TACTIC EXTEND Lia
-[ "xlia" tactic(t) ] -> [   (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) ]
+| [ "xlia" tactic(t) ] -> {   (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND Nia
-[ "xnlia" tactic(t) ] -> [  (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) ]
+| [ "xnlia" tactic(t) ] -> {  (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND NRA
-[ "xnra" tactic(t) ] -> [  (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))]
+| [ "xnra" tactic(t) ] -> {  (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))}
 END
 
 TACTIC EXTEND NQA
-[ "xnqa" tactic(t) ] -> [  (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))]
+| [ "xnqa" tactic(t) ] -> {  (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))}
 END
 
 
   
 TACTIC EXTEND Sos_Z
-| [ "sos_Z" tactic(t) ] -> [ (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) ]
+| [ "sos_Z" tactic(t) ] -> { (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) }
    END
 
 TACTIC EXTEND Sos_Q
-| [ "sos_Q" tactic(t) ] -> [   (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) ]
+| [ "sos_Q" tactic(t) ] -> {   (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) }
    END
 
 TACTIC EXTEND Sos_R
-| [ "sos_R" tactic(t) ] -> [   (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) ]
+| [ "sos_R" tactic(t) ] -> {   (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND LRA_Q
-[ "lra_Q"  tactic(t) ] -> [   (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) ]
+| [ "lra_Q"  tactic(t) ] -> {   (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND LRA_R
-[ "lra_R" tactic(t) ] -> [   (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) ]
+| [ "lra_R" tactic(t) ] -> {   (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) tactic(t) ] -> [   (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) ]
-| [ "psatz_R" tactic(t) ] -> [   (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) ]
+| [ "psatz_R" int_or_var(i) tactic(t) ] -> {   (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_R" tactic(t) ] -> {   (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND PsatzQ
-| [ "psatz_Q" int_or_var(i) tactic(t) ] -> [  (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) ]
-| [ "psatz_Q" tactic(t) ] -> [  (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) ]
+| [ "psatz_Q" int_or_var(i) tactic(t) ] -> {  (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_Q" tactic(t) ] -> {  (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) }
 END
 
diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli
index 7b7a090de0..094429ea18 100644
--- a/plugins/micromega/mutils.mli
+++ b/plugins/micromega/mutils.mli
@@ -30,7 +30,7 @@ end
 
 module TagSet : CSig.SetS with type elt = Tag.t
 
-val pp_list : (out_channel -> 'a -> 'b) -> out_channel -> 'a list -> unit
+val pp_list : (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit
 
 module CamlToCoq : sig