20 files changed, 149 insertions, 1210 deletions

diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
deleted file mode 100644
index 07f32be8e..000000000
--- a/plugins/fourier/Fourier.v
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* "Fourier's method to solve linear inequations/equations systems.".*)
-
-Require Export Field.
-Require Export DiscrR.
-Require Export Fourier_util.
-Declare ML Module "fourier_plugin".
-
-Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR).
-
-Ltac fourier_eq := apply Rge_antisym; fourier.
diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v
deleted file mode 100644
index d3159698b..000000000
--- a/plugins/fourier/Fourier_util.v
+++ /dev/null
@@ -1,222 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-Require Export Rbase.
-Comments "Lemmas used by the tactic Fourier".
-
-Open Scope R_scope.
-
-Lemma Rfourier_lt : forall x1 y1 a:R, x1 < y1 -> 0 < a -> a * x1 < a * y1.
-intros; apply Rmult_lt_compat_l; assumption.
-Qed.
-
-Lemma Rfourier_le : forall x1 y1 a:R, x1 <= y1 -> 0 < a -> a * x1 <= a * y1.
-red.
-intros.
-case H; auto with real.
-Qed.
-
-Lemma Rfourier_lt_lt :
- forall x1 y1 x2 y2 a:R,
-   x1 < y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
-intros x1 y1 x2 y2 a H H0 H1; try assumption.
-apply Rplus_lt_compat.
-try exact H.
-apply Rfourier_lt.
-try exact H0.
-try exact H1.
-Qed.
-
-Lemma Rfourier_lt_le :
- forall x1 y1 x2 y2 a:R,
-   x1 < y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
-intros x1 y1 x2 y2 a H H0 H1; try assumption.
-case H0; intros.
-apply Rplus_lt_compat.
-try exact H.
-apply Rfourier_lt; auto with real.
-rewrite H2.
-rewrite (Rplus_comm y1 (a * y2)).
-rewrite (Rplus_comm x1 (a * y2)).
-apply Rplus_lt_compat_l.
-try exact H.
-Qed.
-
-Lemma Rfourier_le_lt :
- forall x1 y1 x2 y2 a:R,
-   x1 <= y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2.
-intros x1 y1 x2 y2 a H H0 H1; try assumption.
-case H; intros.
-apply Rfourier_lt_le; auto with real.
-rewrite H2.
-apply Rplus_lt_compat_l.
-apply Rfourier_lt; auto with real.
-Qed.
-
-Lemma Rfourier_le_le :
- forall x1 y1 x2 y2 a:R,
-   x1 <= y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 <= y1 + a * y2.
-intros x1 y1 x2 y2 a H H0 H1; try assumption.
-case H0; intros.
-red.
-left; try assumption.
-apply Rfourier_le_lt; auto with real.
-rewrite H2.
-case H; intros.
-red.
-left; try assumption.
-rewrite (Rplus_comm x1 (a * y2)).
-rewrite (Rplus_comm y1 (a * y2)).
-apply Rplus_lt_compat_l.
-try exact H3.
-rewrite H3.
-red.
-right; try assumption.
-auto with real.
-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 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_1 : 0 < 1.
-exact Rlt_0_1.
-Qed.
-
-Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x.
-intros x H; try assumption.
-case H; intros.
-red.
-left; try assumption.
-apply Rlt_zero_pos_plus1; auto with real.
-rewrite <- H0.
-replace (1 + 0) with 1.
-red; left.
-exact Rlt_zero_1.
-ring.
-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.
-
-Lemma Rle_zero_1 : 0 <= 1.
-red; left.
-exact Rlt_zero_1.
-Qed.
-
-Lemma Rle_not_lt : forall n d:R, 0 <= n * / d -> ~ 0 < - n * / d.
-intros n d H; red; intros H0; try exact H0.
-generalize (Rgt_not_le 0 (n * / d)).
-intros H1; elim H1; try assumption.
-replace (n * / d) with (- - (n * / d)).
-replace 0 with (- -0).
-replace (- (n * / d)) with (- n * / d).
-replace (-0) with 0.
-red.
-apply Ropp_gt_lt_contravar.
-red.
-exact H0.
-ring.
-ring.
-ring.
-ring.
-Qed.
-
-Lemma Rnot_lt0 : forall x:R, ~ 0 < 0 * x.
-intros x; try assumption.
-replace (0 * x) with 0.
-apply Rlt_irrefl.
-ring.
-Qed.
-
-Lemma Rlt_not_le_frac_opp : forall n d:R, 0 < n * / d -> ~ 0 <= - n * / d.
-intros n d H; try assumption.
-apply Rgt_not_le.
-replace 0 with (-0).
-replace (- n * / d) with (- (n * / d)).
-apply Ropp_lt_gt_contravar.
-try exact H.
-ring.
-ring.
-Qed.
-
-Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y.
-unfold not; intros.
-apply H.
-apply Rplus_lt_reg_l with x.
-replace (x + 0) with x.
-replace (x + (y - x)) with y.
-try exact H0.
-ring.
-ring.
-Qed.
-
-Lemma Rnot_le_le : forall x y:R, ~ 0 <= y - x -> ~ x <= y.
-unfold not; intros.
-apply H.
-case H0; intros.
-left.
-apply Rplus_lt_reg_l with x.
-replace (x + 0) with x.
-replace (x + (y - x)) with y.
-try exact H1.
-ring.
-ring.
-right.
-rewrite H1; ring.
-Qed.
-
-Lemma Rfourier_gt_to_lt : forall x y:R, y > x -> x < y.
-unfold Rgt; intros; assumption.
-Qed.
-
-Lemma Rfourier_ge_to_le : forall x y:R, y >= x -> x <= y.
-intros x y; exact (Rge_le y x).
-Qed.
-
-Lemma Rfourier_eqLR_to_le : forall x y:R, x = y -> x <= y.
-exact Req_le.
-Qed.
-
-Lemma Rfourier_eqRL_to_le : forall x y:R, y = x -> x <= y.
-exact Req_le_sym.
-Qed.
-
-Lemma Rfourier_not_ge_lt : forall x y:R, (x >= y -> False) -> x < y.
-exact Rnot_ge_lt.
-Qed.
-
-Lemma Rfourier_not_gt_le : forall x y:R, (x > y -> False) -> x <= y.
-exact Rnot_gt_le.
-Qed.
-
-Lemma Rfourier_not_le_gt : forall x y:R, (x <= y -> False) -> x > y.
-exact Rnot_le_lt.
-Qed.
-
-Lemma Rfourier_not_lt_ge : forall x y:R, (x < y -> False) -> x >= y.
-exact Rnot_lt_ge.
-Qed.
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
deleted file mode 100644
index bee2b3b58..000000000
--- a/plugins/fourier/fourier.ml
+++ /dev/null
@@ -1,204 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Méthode d'élimination de Fourier *)
-(* Référence:
-Auteur(s) : Fourier, Jean-Baptiste-Joseph
-
-Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,...
-
-Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890
-
-Pages: 326-327
-
-http://gallica.bnf.fr/
-*)
-
-(* Un peu de calcul sur les rationnels...
-Les opérations rendent des rationnels normalisés,
-i.e. le numérateur et le dénominateur sont premiers entre eux.
-*)
-type rational = {num:int;
-                 den:int}
-;;
-let print_rational x =
-        print_int x.num;
-        print_string "/";
-        print_int x.den
-;;
-
-let rec pgcd x y = if y = 0 then x else pgcd y (x mod y);;
-
-
-let r0 = {num=0;den=1};;
-let r1 = {num=1;den=1};;
-
-let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in
-              if x.num=0 then r0
-              else (let d=pgcd x.num x.den in
-		    let d= (if d<0 then -d else d) in
-                    {num=(x.num)/d;den=(x.den)/d});;
-
-let rop x = rnorm {num=(-x.num);den=x.den};;
-
-let rplus x y = rnorm {num=x.num*y.den + y.num*x.den;den=x.den*y.den};;
-
-let rminus x y = rnorm {num=x.num*y.den - y.num*x.den;den=x.den*y.den};;
-
-let rmult x y = rnorm {num=x.num*y.num;den=x.den*y.den};;
-
-let rinv x = rnorm {num=x.den;den=x.num};;
-
-let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};;
-
-let rinf x y = x.num*y.den < y.num*x.den;;
-let rinfeq x y = x.num*y.den <= y.num*x.den;;
-
-(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation
-c1x1+...+cnxn < d si strict=true, <= sinon,
-hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ.
-*)
-
-type ineq = {coef:rational list;
-             hist:rational list;
-             strict:bool};;
-
-let pop x l = l:=x::(!l);;
-
-(* sépare la liste d'inéquations s selon que leur premier coefficient est
-négatif, nul ou positif. *)
-let partitionne s =
-   let lpos=ref [] in
-   let lneg=ref [] in
-   let lnul=ref [] in
-   List.iter (fun ie -> match ie.coef with
-                        [] ->  raise (Failure "empty ineq")
-                       |(c::r) -> if rinf c r0
-           	                  then pop ie lneg
-                                  else if rinf r0 c then pop ie lpos
-                                              else pop ie lnul)
-             s;
-   [!lneg;!lnul;!lpos]
-;;
-(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!):
-(add_hist [(equation 1, s1);...;(équation n, sn)])
-=
-[{équation 1, [1;0;...;0], s1};
- {équation 2, [0;1;...;0], s2};
- ...
- {équation n, [0;0;...;1], sn}]
-*)
-let add_hist le =
-   let n = List.length le in
-   let i = ref 0 in
-   List.map (fun (ie,s) ->
-              let h = ref [] in
-              for _k = 1 to (n - (!i) - 1) do pop r0 h; done;
-              pop r1 h;
-              for _k = 1 to !i do pop r0 h; done;
-              i:=!i+1;
-              {coef=ie;hist=(!h);strict=s})
-             le
-;;
-(* additionne deux inéquations *)
-let ie_add ie1 ie2 = {coef=List.map2 rplus ie1.coef ie2.coef;
-                      hist=List.map2 rplus ie1.hist ie2.hist;
-		      strict=ie1.strict || ie2.strict}
-;;
-(* multiplication d'une inéquation par un rationnel (positif) *)
-let ie_emult a ie = {coef=List.map (fun x -> rmult a x) ie.coef;
-                     hist=List.map (fun x -> rmult a x) ie.hist;
-		     strict= ie.strict}
-;;
-(* on enlève le premier coefficient *)
-let ie_tl ie = {coef=List.tl ie.coef;hist=ie.hist;strict=ie.strict}
-;;
-(* le premier coefficient: "tête" de l'inéquation *)
-let hd_coef ie = List.hd ie.coef
-;;
-
-(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient.
-*)
-let deduce_add lneg lpos =
-   let res=ref [] in
-   List.iter (fun i1 ->
-		 List.iter (fun i2 ->
-				let a = rop (hd_coef i1) in
-				let b = hd_coef i2 in
-				pop (ie_tl (ie_add (ie_emult b i1)
-						   (ie_emult a i2))) res)
-		           lpos)
-             lneg;
-   !res
-;;
-(* élimination de la première variable à partir d'une liste d'inéquations:
-opération qu'on itère dans l'algorithme de Fourier.
-*)
-let deduce1 s =
-    match (partitionne s) with
-      [lneg;lnul;lpos] ->
-    let lnew = deduce_add lneg lpos in
-    (List.map ie_tl lnul)@lnew
-     |_->assert false
-;;
-(* algorithme de Fourier: on élimine successivement toutes les variables.
-*)
-let deduce lie =
-   let n = List.length (fst (List.hd lie)) in
-   let lie=ref (add_hist lie) in
-   for _i = 1 to n - 1 do
-      lie:= deduce1 !lie;
-   done;
-   !lie
-;;
-
-(* donne [] si le système a des solutions,
-sinon donne [c,s,lc]
-où lc est la combinaison linéaire des inéquations de départ
-qui donne 0 < c si s=true
-       ou 0 <= c sinon
-cette inéquation étant absurde.
-*)
-
-exception Contradiction of (rational * bool * rational list) list
-
-let unsolvable lie =
-   let lr = deduce lie in
-   let check = function
-     | {coef=[c];hist=lc;strict=s} ->
-       if (rinf c r0 && (not s)) || (rinfeq c r0 && s)
-       then raise (Contradiction [c,s,lc])
-     |_->assert false
-   in
-   try List.iter check lr; []
-   with Contradiction l -> l
-
-(* Exemples:
-
-let test1=[[r1;r1;r0],true;[rop r1;r1;r1],false;[r0;rop r1;rop r1],false];;
-deduce test1;;
-unsolvable test1;;
-
-let test2=[
-[r1;r1;r0;r0;r0],false;
-[r0;r1;r1;r0;r0],false;
-[r0;r0;r1;r1;r0],false;
-[r0;r0;r0;r1;r1],false;
-[r1;r0;r0;r0;r1],false;
-[rop r1;rop r1;r0;r0;r0],false;
-[r0;rop r1;rop r1;r0;r0],false;
-[r0;r0;rop r1;rop r1;r0],false;
-[r0;r0;r0;rop r1;rop r1],false;
-[rop r1;r0;r0;r0;rop r1],false
-];;
-deduce test2;;
-unsolvable test2;;
-
-*)
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
deleted file mode 100644
index 96be1d893..000000000
--- a/plugins/fourier/fourierR.ml
+++ /dev/null
@@ -1,644 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-
-
-(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
-des inéquations et équations sont entiers. En attendant la tactique Field.
-*)
-
-open Constr
-open Tactics
-open Names
-open Globnames
-open Fourier
-open Contradiction
-open Proofview.Notations
-
-(******************************************************************************
-Opérations sur les combinaisons linéaires affines.
-La partie homogène d'une combinaison linéaire est en fait une table de hash
-qui donne le coefficient d'un terme du calcul des constructions,
-qui est zéro si le terme n'y est pas.
-*)
-
-module Constrhash = Hashtbl.Make(Constr)
-
-type flin = {fhom: rational Constrhash.t;
-             fcste:rational};;
-
-let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};;
-
-let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;;
-
-let flin_add f x c =
-    let cx = flin_coef f x in
-    Constrhash.replace f.fhom x (rplus cx c);
-    f
-;;
-let flin_add_cste f c =
-    {fhom=f.fhom;
-     fcste=rplus f.fcste c}
-;;
-
-let flin_one () = flin_add_cste (flin_zero()) r1;;
-
-let flin_plus f1 f2 =
-    let f3 = flin_zero() in
-    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
-    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
-    flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
-;;
-
-let flin_minus f1 f2 =
-    let f3 = flin_zero() in
-    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
-    Constrhash.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
-    flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
-;;
-let flin_emult a f =
-    let f2 = flin_zero() in
-    Constrhash.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
-    flin_add_cste f2 (rmult a f.fcste);
-;;
-
-(*****************************************************************************)
-
-type ineq = Rlt | Rle | Rgt | Rge
-
-let string_of_R_constant kn =
-  match Constant.repr3 kn with
-    | ModPath.MPfile dir, sec_dir, id when
-	sec_dir = DirPath.empty &&
-	DirPath.to_string dir = "Coq.Reals.Rdefinitions"
-	-> Label.to_string id
-    | _ -> "constant_not_of_R"
-
-let rec string_of_R_constr c =
- match Constr.kind c with
-   Cast (c,_,_) -> string_of_R_constr c
-  |Const (c,_) -> string_of_R_constant c
-  | _ -> "not_of_constant"
-
-exception NoRational
-
-let rec rational_of_constr c =
-  match Constr.kind c with
-  | Cast (c,_,_) -> (rational_of_constr c)
-  | App (c,args) ->
-      (match (string_of_R_constr c) with
-	 | "Ropp" ->
-	     rop (rational_of_constr args.(0))
-	 | "Rinv" ->
-	     rinv (rational_of_constr args.(0))
-	 | "Rmult" ->
-	     rmult (rational_of_constr args.(0))
-                   (rational_of_constr args.(1))
-	 | "Rdiv" ->
-	     rdiv (rational_of_constr args.(0))
-                  (rational_of_constr args.(1))
-	 | "Rplus" ->
-	     rplus (rational_of_constr args.(0))
-                   (rational_of_constr args.(1))
-	 | "Rminus" ->
-	     rminus (rational_of_constr args.(0))
-                    (rational_of_constr args.(1))
-	 | _ -> raise NoRational)
-  | Const (kn,_) ->
-      (match (string_of_R_constant kn) with
-	       "R1" -> r1
-              |"R0" -> r0
-              |  _ -> raise NoRational)
-  |  _ -> raise NoRational
-;;
-
-exception NoLinear
-
-let rec flin_of_constr c =
-  try(
-    match Constr.kind c with
-  | Cast (c,_,_) -> (flin_of_constr c)
-  | App (c,args) ->
-      (match (string_of_R_constr c) with
-	   "Ropp" ->
-             flin_emult (rop r1) (flin_of_constr args.(0))
-	 | "Rplus"->
-             flin_plus (flin_of_constr args.(0))
-	               (flin_of_constr args.(1))
-	 | "Rminus"->
-             flin_minus (flin_of_constr args.(0))
-	                (flin_of_constr args.(1))
-	 | "Rmult"->
-	     (try
-                let a = rational_of_constr args.(0) in
-                try
-                  let b = rational_of_constr args.(1) in
-		  flin_add_cste (flin_zero()) (rmult a b)
-		with NoRational ->
-                  flin_add (flin_zero()) args.(1) a
-	      with NoRational ->
-                flin_add (flin_zero()) args.(0)
-		  (rational_of_constr args.(1)))
-	 | "Rinv"->
-	     let a = rational_of_constr args.(0) in
-	     flin_add_cste (flin_zero()) (rinv a)
-	 | "Rdiv"->
-	     (let b = rational_of_constr args.(1) in
-	      try
-                let a = rational_of_constr args.(0) in
-	        flin_add_cste (flin_zero()) (rdiv a b)
-	      with NoRational ->
-                flin_add (flin_zero()) args.(0) (rinv b))
-         |_-> raise NoLinear)
-  | Const (c,_) ->
-        (match (string_of_R_constant c) with
-	       "R1" -> flin_one ()
-              |"R0" -> flin_zero ()
-              |_-> raise NoLinear)
-  |_-> raise NoLinear)
-  with NoRational | NoLinear -> flin_add (flin_zero()) c r1
-;;
-
-let flin_to_alist f =
-    let res=ref [] in
-    Constrhash.iter (fun x c -> res:=(c,x)::(!res)) f;
-    !res
-;;
-
-(* Représentation des hypothèses qui sont des inéquations ou des équations.
-*)
-type hineq={hname:constr; (* le nom de l'hypothèse *)
-            htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
-            hleft:constr;
-            hright:constr;
-            hflin:flin;
-            hstrict:bool}
-;;
-
-(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
-*)
-
-exception NoIneq
-
-let ineq1_of_constr (h,t) =
-  let h = EConstr.Unsafe.to_constr h in
-  let t = EConstr.Unsafe.to_constr t in
-    match (Constr.kind t) with
-      | App (f,args) ->
-        (match Constr.kind f with
-          | Const (c,_) when Array.length args = 2 ->
-            let t1= args.(0) in
-            let t2= args.(1) in
-            (match (string_of_R_constant c) with
-	      |"Rlt" -> [{hname=h;
-                           htype="Rlt";
-		           hleft=t1;
-			   hright=t2;
-			   hflin= flin_minus (flin_of_constr t1)
-                                             (flin_of_constr t2);
-			   hstrict=true}]
-	      |"Rgt" -> [{hname=h;
-                           htype="Rgt";
-		           hleft=t2;
-			   hright=t1;
-			   hflin= flin_minus (flin_of_constr t2)
-                                             (flin_of_constr t1);
-			   hstrict=true}]
-	      |"Rle" -> [{hname=h;
-                           htype="Rle";
-		           hleft=t1;
-			   hright=t2;
-			   hflin= flin_minus (flin_of_constr t1)
-                                             (flin_of_constr t2);
-			   hstrict=false}]
-	      |"Rge" -> [{hname=h;
-                           htype="Rge";
-		           hleft=t2;
-			   hright=t1;
-			   hflin= flin_minus (flin_of_constr t2)
-                                             (flin_of_constr t1);
-			   hstrict=false}]
-              |_-> raise NoIneq)
-          | Ind ((kn,i),_) ->
-            if not (GlobRef.equal (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq;
-            let t0= args.(0) in
-            let t1= args.(1) in
-            let t2= args.(2) in
-	    (match (Constr.kind t0) with
-              | Const (c,_) ->
-		(match (string_of_R_constant c) with
-		  | "R"->
-                         [{hname=h;
-                           htype="eqTLR";
-		           hleft=t1;
-			   hright=t2;
-			   hflin= flin_minus (flin_of_constr t1)
-                                             (flin_of_constr t2);
-			   hstrict=false};
-                          {hname=h;
-                           htype="eqTRL";
-		           hleft=t2;
-			   hright=t1;
-			   hflin= flin_minus (flin_of_constr t2)
-                                             (flin_of_constr t1);
-			   hstrict=false}]
-                  |_-> raise NoIneq)
-              |_-> raise NoIneq)
-          |_-> raise NoIneq)
-      |_-> raise NoIneq
-;;
-
-(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
-*)
-
-let fourier_lineq lineq1 =
-   let nvar=ref (-1) in
-   let hvar=Constrhash.create 50 in (* la table des variables des inéquations *)
-   List.iter (fun f ->
-		Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin
-				nvar:=(!nvar)+1;
-				Constrhash.add hvar x (!nvar)
-			      end)
-                  f.hflin.fhom)
-             lineq1;
-   let sys= List.map (fun h->
-               let v=Array.make ((!nvar)+1) r0 in
-               Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c)
-                  h.hflin.fhom;
-               ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
-             lineq1 in
-   unsolvable sys
-;;
-
-(*********************************************************************)
-(* Defined constants *)
-
-let get = Lazy.force
-let cget = get
-let eget c = EConstr.of_constr (Lazy.force c)
-let constant path s = UnivGen.constr_of_global @@
-  Coqlib.coq_reference "Fourier" path s
-
-(* Standard library *)
-open Coqlib
-let coq_sym_eqT = lazy (build_coq_eq_sym ())
-let coq_False = lazy (UnivGen.constr_of_global @@ build_coq_False ())
-let coq_not = lazy (UnivGen.constr_of_global @@ build_coq_not ())
-let coq_eq = lazy (UnivGen.constr_of_global @@ build_coq_eq ())
-
-(* Rdefinitions *)
-let constant_real = constant ["Reals";"Rdefinitions"]
-
-let coq_Rlt = lazy (constant_real "Rlt")
-let coq_Rgt = lazy (constant_real "Rgt")
-let coq_Rle = lazy (constant_real "Rle")
-let coq_Rge = lazy (constant_real "Rge")
-let coq_R = lazy (constant_real "R")
-let coq_Rminus = lazy (constant_real "Rminus")
-let coq_Rmult = lazy (constant_real "Rmult")
-let coq_Rplus = lazy (constant_real "Rplus")
-let coq_Ropp = lazy (constant_real "Ropp")
-let coq_Rinv = lazy (constant_real "Rinv")
-let coq_R0 = lazy (constant_real "R0")
-let coq_R1 = lazy (constant_real "R1")
-
-(* RIneq *)
-let coq_Rinv_1 = lazy (constant ["Reals";"RIneq"] "Rinv_1")
-
-(* Fourier_util *)
-let constant_fourier = constant ["fourier";"Fourier_util"]
-
-let coq_Rlt_zero_1 = lazy (constant_fourier "Rlt_zero_1")
-let coq_Rlt_zero_pos_plus1 = lazy (constant_fourier "Rlt_zero_pos_plus1")
-let coq_Rle_zero_pos_plus1 = lazy (constant_fourier "Rle_zero_pos_plus1")
-let coq_Rlt_mult_inv_pos = lazy (constant_fourier "Rlt_mult_inv_pos")
-let coq_Rle_zero_zero = lazy (constant_fourier "Rle_zero_zero")
-let coq_Rle_zero_1 = lazy (constant_fourier "Rle_zero_1")
-let coq_Rle_mult_inv_pos = lazy (constant_fourier "Rle_mult_inv_pos")
-let coq_Rnot_lt0 = lazy (constant_fourier "Rnot_lt0")
-let coq_Rle_not_lt = lazy (constant_fourier "Rle_not_lt")
-let coq_Rfourier_gt_to_lt = lazy (constant_fourier "Rfourier_gt_to_lt")
-let coq_Rfourier_ge_to_le = lazy (constant_fourier "Rfourier_ge_to_le")
-let coq_Rfourier_eqLR_to_le = lazy (constant_fourier "Rfourier_eqLR_to_le")
-let coq_Rfourier_eqRL_to_le = lazy (constant_fourier "Rfourier_eqRL_to_le")
-
-let coq_Rfourier_not_ge_lt = lazy (constant_fourier "Rfourier_not_ge_lt")
-let coq_Rfourier_not_gt_le = lazy (constant_fourier "Rfourier_not_gt_le")
-let coq_Rfourier_not_le_gt = lazy (constant_fourier "Rfourier_not_le_gt")
-let coq_Rfourier_not_lt_ge = lazy (constant_fourier "Rfourier_not_lt_ge")
-let coq_Rfourier_lt = lazy (constant_fourier "Rfourier_lt")
-let coq_Rfourier_le = lazy (constant_fourier "Rfourier_le")
-let coq_Rfourier_lt_lt = lazy (constant_fourier "Rfourier_lt_lt")
-let coq_Rfourier_lt_le = lazy (constant_fourier "Rfourier_lt_le")
-let coq_Rfourier_le_lt = lazy (constant_fourier "Rfourier_le_lt")
-let coq_Rfourier_le_le = lazy (constant_fourier "Rfourier_le_le")
-let coq_Rnot_lt_lt = lazy (constant_fourier "Rnot_lt_lt")
-let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le")
-let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp")
-
-(******************************************************************************
-Construction de la preuve en cas de succès de la méthode de Fourier,
-i.e. on obtient une contradiction.
-*)
-let is_int x = (x.den)=1
-;;
-
-(* fraction = couple (num,den) *)
-let rational_to_fraction x= (x.num,x.den)
-;;
-
-(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
-*)
-let int_to_real n =
-   let nn=abs n in
-   if nn=0
-   then get coq_R0
-   else
-     (let s=ref (get coq_R1) in
-      for _i = 1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done;
-      if n<0 then mkApp (get coq_Ropp, [|!s|]) else !s)
-;;
-(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
-*)
-let rational_to_real x =
-   let (n,d)=rational_to_fraction x in
-   mkApp (get coq_Rmult,
-     [|int_to_real n;mkApp(get coq_Rinv,[|int_to_real d|])|])
-;;
-
-(* preuve que 0<n*1/d
-*)
-let tac_zero_inf_pos gl (n,d) =
-  let get = eget in
-   let tacn=ref (apply (get coq_Rlt_zero_1)) in
-   let tacd=ref (apply (get coq_Rlt_zero_1)) in
-   for _i = 1 to n - 1 do
-       tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
-   for _i = 1 to d - 1 do
-       tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
-   (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd])
-;;
-
-(* preuve que 0<=n*1/d
-*)
-let tac_zero_infeq_pos gl (n,d)=
-  let get = eget in
-   let tacn=ref (if n=0
-                 then (apply (get coq_Rle_zero_zero))
-                 else (apply (get coq_Rle_zero_1))) in
-   let tacd=ref (apply (get coq_Rlt_zero_1)) in
-   for  _i = 1 to n - 1 do
-       tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
-   for _i = 1 to d - 1 do
-       tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
-   (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
-;;
-
-(* preuve que 0<(-n)*(1/d) => False
-*)
-let tac_zero_inf_false gl (n,d) =
-      let get = eget in
-if n=0 then (apply (get coq_Rnot_lt0))
-    else
-     (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt))
-	      (tac_zero_infeq_pos gl (-n,d)))
-;;
-
-(* preuve que 0<=(-n)*(1/d) => False
-*)
-let tac_zero_infeq_false gl (n,d) =
-  let get = eget in
-     (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
-	      (tac_zero_inf_pos gl (-n,d)))
-;;
-
-let exact = exact_check;;
-
-let tac_use h =
-  let get = eget in
-  let tac = exact (EConstr.of_constr h.hname) in
-  match h.htype with
-    "Rlt" -> tac
-  |"Rle" -> tac
-  |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac)
-  |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac)
-  |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac)
-  |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac)
-  |_->assert false
-;;
-
-(*
-let is_ineq (h,t) =
-    match (Constr.kind t) with
-	App (f,args) ->
-	  (match (string_of_R_constr f) with
-	       "Rlt" -> true
-	     | "Rgt" -> true
-	     | "Rle" -> true
-	     | "Rge" -> true
-(* Wrong:not in Rdefinitions: *) | "eqT" ->
-                (match (string_of_R_constr args.(0)) with
-			     "R" -> true
-			   | _ -> false)
-             | _ ->false)
-      |_->false
-;;
-*)
-
-let list_of_sign s =
-  let open Context.Named.Declaration in
-  List.map (function LocalAssum (name, typ) -> name, typ
-                   | LocalDef (name, _, typ) -> name, typ)
-           s;;
-
-let mkAppL a =
-   let l = Array.to_list a in
-   mkApp(List.hd l, Array.of_list (List.tl l))
-;;
-
-exception GoalDone
-
-(* Résolution d'inéquations linéaires dans R *)
-let rec fourier () =
-  Proofview.Goal.nf_enter begin fun gl ->
-    let concl = Proofview.Goal.concl gl in
-    let sigma = Tacmach.New.project gl in
-    Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
-    let goal = Termops.strip_outer_cast sigma concl in
-    let goal = EConstr.Unsafe.to_constr goal in
-    let fhyp=Id.of_string "new_hyp_for_fourier" in
-    (* si le but est une inéquation, on introduit son contraire,
-       et le but à prouver devient False *)
-    try 
-      match (Constr.kind goal) with
-      App (f,args) ->
-      let get = eget in
-      (match (string_of_R_constr f) with
-	     "Rlt" ->
-	       (Tacticals.New.tclTHEN
-	         (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt))
-			  (intro_using  fhyp))
-		 (fourier ()))
-	    |"Rle" ->
-	     (Tacticals.New.tclTHEN
-	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le))
-		       (intro_using  fhyp))
-			(fourier ()))
-	    |"Rgt" ->
-	     (Tacticals.New.tclTHEN
-	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt))
-		       (intro_using  fhyp))
-	      (fourier ()))
-	    |"Rge" ->
-	     (Tacticals.New.tclTHEN
-	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge))
-		       (intro_using  fhyp))
-	      (fourier ()))
-	    |_-> raise GoalDone)
-        |_-> raise GoalDone
-     with GoalDone ->
-    (* les hypothèses *)
-    let hyps = List.map (fun (h,t)-> (EConstr.mkVar h,t))
-                        (list_of_sign (Proofview.Goal.hyps gl)) in
-    let lineq =ref [] in
-    List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
-		        with NoIneq -> ())
-              hyps;
-    (* lineq = les inéquations découlant des hypothèses *)
-    if !lineq=[] then CErrors.user_err Pp.(str "No inequalities");
-    let res=fourier_lineq (!lineq) in
-    let tac=ref (Proofview.tclUNIT ()) in
-    if res=[]
-    then CErrors.user_err Pp.(str "fourier failed")
-    (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
-    else (match res with
-        [(cres,sres,lc)]->
-    (* lc=coefficients multiplicateurs des inéquations
-       qui donnent 0<cres ou 0<=cres selon sres *)
-	(*print_string "Fourier's method can prove the goal...";flush stdout;*)
-          let lutil=ref [] in
-	  List.iter
-            (fun (h,c) ->
-			  if c<>r0
-        		  then (lutil:=(h,c)::(!lutil)(*;
-				print_rational(c);print_string " "*)))
-                    (List.combine (!lineq) lc);
-       (* on construit la combinaison linéaire des inéquation *)
-             (match (!lutil) with
-          (h1,c1)::lutil ->
-	  let s=ref (h1.hstrict) in
-	  let t1=ref (mkAppL [|get coq_Rmult;
-	                  rational_to_real c1;
-			  h1.hleft|]) in
-	  let t2=ref (mkAppL [|get coq_Rmult;
-	                  rational_to_real c1;
-			  h1.hright|]) in
-	  List.iter (fun (h,c) ->
-	       s:=(!s)||(h.hstrict);
-	       t1:=(mkAppL [|get coq_Rplus;
-	                     !t1;
-                             mkAppL [|get coq_Rmult;
-                                      rational_to_real c;
-			              h.hleft|] |]);
-	       t2:=(mkAppL [|get coq_Rplus;
-	                     !t2;
-                             mkAppL [|get coq_Rmult;
-                                      rational_to_real c;
-			              h.hright|] |]))
-               lutil;
-          let ineq=mkAppL [|if (!s) then get coq_Rlt else get coq_Rle;
-			      !t1;
-			      !t2 |] in
-	   let tc=rational_to_real cres in
-       (* puis sa preuve *)
-          let get = eget in
-           let tac1=ref (if h1.hstrict
-                         then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt))
-                                 [tac_use h1;
-                                  tac_zero_inf_pos  gl
-                                      (rational_to_fraction c1)])
-                         else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le))
-                                 [tac_use h1;
-				  tac_zero_inf_pos  gl
-                                      (rational_to_fraction c1)])) in
-           s:=h1.hstrict;
-           List.iter (fun (h,c)->
-             (if (!s)
-	      then (if h.hstrict
-	            then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt))
-			       [!tac1;tac_use h;
-			        tac_zero_inf_pos  gl
-                                      (rational_to_fraction c)])
-	            else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le))
-			       [!tac1;tac_use h;
-			        tac_zero_inf_pos  gl
-                                      (rational_to_fraction c)]))
-	      else (if h.hstrict
-	            then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt))
-			       [!tac1;tac_use h;
-			        tac_zero_inf_pos  gl
-                                      (rational_to_fraction c)])
-	            else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le))
-			       [!tac1;tac_use h;
-			        tac_zero_inf_pos  gl
-                                      (rational_to_fraction c)])));
-	     s:=(!s)||(h.hstrict))
-              lutil;
-           let tac2= if sres
-                      then tac_zero_inf_false gl (rational_to_fraction cres)
-                      else tac_zero_infeq_false gl (rational_to_fraction cres)
-           in
-           tac:=(Tacticals.New.tclTHENS (cut (EConstr.of_constr ineq))
-                     [Tacticals.New.tclTHEN (change_concl
-			       (EConstr.of_constr (mkAppL [| cget coq_not; ineq|]
-				       )))
-		      (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
-					       else get coq_Rnot_le_le))
-			    (Tacticals.New.tclTHENS (Equality.replace
-				       (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|]
-					       ))
-				       (EConstr.of_constr tc))
-		 	       [tac2;
-                                (Tacticals.New.tclTHENS
-				  (Equality.replace
-				    (EConstr.of_constr (mkApp (cget coq_Rinv,
-				      [|cget coq_R1|])))
-				    (get coq_R1))
-(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
-
-      			        [Tacticals.New.tclORELSE
-                                   (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
-                                   (Proofview.tclUNIT ());
-				 Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq ->
-					  (Tacticals.New.tclTHEN (apply symeq)
-						(apply (get coq_Rinv_1)))]
-
-					 )
-				]));
-                       !tac1]);
-	   tac:=(Tacticals.New.tclTHENS (cut (get coq_False))
-				  [Tacticals.New.tclTHEN intro (contradiction None);
-				   !tac])
-      |_-> assert false) |_-> assert false
-	  );
-(*    ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
-      !tac
-(*      ((tclABSTRACT None !tac) gl) *)
-  end
-;;
-
-(*
-let fourier_tac x gl =
-     fourier gl
-;;
-
-let v_fourier = add_tactic "Fourier" fourier_tac
-*)
-
diff --git a/plugins/fourier/fourier_plugin.mlpack b/plugins/fourier/fourier_plugin.mlpack
deleted file mode 100644
index b6262f8ae..000000000
--- a/plugins/fourier/fourier_plugin.mlpack
+++ /dev/null
@@ -1,3 +0,0 @@
-Fourier
-FourierR
-G_fourier
diff --git a/plugins/fourier/g_fourier.mlg b/plugins/fourier/g_fourier.mlg
deleted file mode 100644
index 703e29f96..000000000
--- a/plugins/fourier/g_fourier.mlg
+++ /dev/null
@@ -1,22 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-{
-
-open Ltac_plugin
-open FourierR
-
-}
-
-DECLARE PLUGIN "fourier_plugin"
-
-TACTIC EXTEND fourier
-| [ "fourierz" ] -> { fourier () }
-END
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index b95d64ce9..549f1fc0e 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -14,6 +14,6 @@ bool ->
            int -> Constrexpr.constr_expr -> (pconstant ->
             Indfun_common.tcc_lemma_value ref ->
             pconstant ->
-            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit
 
 
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index dae2582bd..dbbdbfa39 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -297,25 +297,6 @@ END
 
 (* spiwack: the print functions are incomplete, but I don't know what they are
 	used for *)
-let pr_r_nat_field natf =
-  str "nat " ++
-  match natf with
-    | Retroknowledge.NatType -> str "type"
-    | Retroknowledge.NatPlus -> str "plus"
-    | Retroknowledge.NatTimes -> str "times"
-
-let pr_r_n_field  nf =
-  str "binary N " ++
-  match nf with
-    | Retroknowledge.NPositive -> str "positive"
-    | Retroknowledge.NType -> str "type"
-    | Retroknowledge.NTwice -> str "twice"
-    | Retroknowledge.NTwicePlusOne -> str "twice plus one"
-    | Retroknowledge.NPhi -> str "phi"
-    | Retroknowledge.NPhiInv -> str "phi inv"
-    | Retroknowledge.NPlus -> str "plus"
-    | Retroknowledge.NTimes -> str "times"
-
 let pr_r_int31_field i31f =
   str "int31 " ++
   match i31f with
@@ -353,26 +334,6 @@ let pr_retroknowledge_field f =
   | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++
                                            spc () ++ str "in " ++ qs group
 
-VERNAC ARGUMENT EXTEND retroknowledge_nat
-PRINTED BY pr_r_nat_field
-| [ "nat" "type" ] -> [ Retroknowledge.NatType ]
-| [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ]
-| [ "nat" "times" ] -> [ Retroknowledge.NatTimes ]
-END
-
-
-VERNAC ARGUMENT EXTEND retroknowledge_binary_n
-PRINTED BY pr_r_n_field
-| [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ]
-| [ "binary" "N" "type" ] -> [ Retroknowledge.NType ]
-| [ "binary" "N" "twice" ] -> [ Retroknowledge.NTwice ]
-| [ "binary" "N" "twice" "plus" "one" ] -> [ Retroknowledge.NTwicePlusOne ]
-| [ "binary" "N" "phi" ] -> [ Retroknowledge.NPhi ]
-| [ "binary" "N" "phi" "inv" ] -> [ Retroknowledge.NPhiInv ]
-| [ "binary" "N" "plus" ] -> [ Retroknowledge.NPlus ]
-| [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ]
-END
-
 VERNAC ARGUMENT EXTEND retroknowledge_int31
 PRINTED BY pr_r_int31_field
 | [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 9d86f21d4..c13bd69da 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -287,12 +287,14 @@ GEXTEND Gram
 
   (* Definitions for tactics *)
   tacdef_body:
-    [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
+    [ [ name = Constr.global; it=LIST1 input_fun;
+        redef = ltac_def_kind; body = tactic_expr ->
           if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
           else
             let id = reference_to_id name in
             Tacexpr.TacticDefinition (id, TacFun (it, body))
-      | name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
+      | name = Constr.global; redef = ltac_def_kind;
+        body = tactic_expr ->
           if redef then Tacexpr.TacticRedefinition (name, body)
           else
             let id = reference_to_id name in
@@ -468,7 +470,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation
   [ VtSideff [], VtNow ] ->
   [ fun ~atts ~st -> let open Vernacinterp in
       let n = Option.default 0 n in
-      Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e;
+      let deprecation = atts.deprecated in
+      Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e;
       st
   ]
 END
@@ -512,7 +515,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
       | TacticDefinition ({CAst.v=r},_) -> r
       | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
   ] -> [ fun ~atts ~st -> let open Vernacinterp in
-           Tacentries.register_ltac (Locality.make_module_locality atts.locality) l;
+           let deprecation = atts.deprecated in
+           Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
            st
   ]
 END
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fac464a62..4b834d66d 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -252,7 +252,7 @@ type tactic_grammar_obj = {
   tacobj_key : KerName.t;
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
-  tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
+  tacobj_body : Tacenv.alias_tactic;
   tacobj_forml : bool;
 }
 
@@ -288,10 +288,11 @@ let load_tactic_notation i (_, tobj) =
     extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
 
 let subst_tactic_notation (subst, tobj) =
-  let (ids, body) = tobj.tacobj_body in
+  let open Tacenv in
+  let alias = tobj.tacobj_body in
   { tobj with
     tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
-    tacobj_body = (ids, Tacsubst.subst_tactic subst body);
+    tacobj_body = { alias with alias_body = Tacsubst.subst_tactic subst alias.alias_body };
   }
 
 let classify_tactic_notation tacobj = Substitute tacobj
@@ -308,25 +309,26 @@ let cons_production_parameter = function
 | TacTerm _ -> None
 | TacNonTerm (_, (_, ido)) -> ido
 
-let add_glob_tactic_notation local ~level prods forml ids tac =
+let add_glob_tactic_notation local ~level ?deprecation prods forml ids tac =
   let parule = {
     tacgram_level = level;
     tacgram_prods = prods;
   } in
+  let open Tacenv in
   let tacobj = {
     tacobj_key = make_fresh_key prods;
     tacobj_local = local;
     tacobj_tacgram = parule;
-    tacobj_body = (ids, tac);
+    tacobj_body = { alias_args = ids; alias_body = tac; alias_deprecation = deprecation };
     tacobj_forml = forml;
   } in
   Lib.add_anonymous_leaf (inTacticGrammar tacobj)
 
-let add_tactic_notation local n prods e =
+let add_tactic_notation local n ?deprecation prods e =
   let ids = List.map_filter cons_production_parameter prods in
   let prods = List.map interp_prod_item prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  add_glob_tactic_notation local ~level:n prods false ids tac
+  add_glob_tactic_notation local ~level:n ?deprecation prods false ids tac
 
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
@@ -366,7 +368,7 @@ let extend_atomic_tactic name entries =
   in
   List.iteri add_atomic entries
 
-let add_ml_tactic_notation name ~level prods =
+let add_ml_tactic_notation name ~level ?deprecation prods =
   let len = List.length prods in
   let iter i prods =
     let open Tacexpr in
@@ -378,7 +380,7 @@ let add_ml_tactic_notation name ~level prods =
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
     let map id = Reference (Locus.ArgVar (CAst.make id)) in
     let tac = TacML (Loc.tag (entry, List.map map ids)) in
-    add_glob_tactic_notation false ~level prods true ids tac
+    add_glob_tactic_notation false ~level ?deprecation prods true ids tac
   in
   List.iteri iter (List.rev prods);
   (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
@@ -430,7 +432,7 @@ let warn_unusable_identifier =
       (fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++
         strbrk "may be unusable because of a conflict with a notation.")
 
-let register_ltac local tacl =
+let register_ltac local ?deprecation tacl =
   let map tactic_body =
     match tactic_body with
     | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
@@ -483,10 +485,10 @@ let register_ltac local tacl =
   let defs = States.with_state_protection defs () in
   let iter (def, tac) = match def with
   | NewTac id ->
-    Tacenv.register_ltac false local id tac;
+    Tacenv.register_ltac false local id tac ?deprecation;
     Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
   | UpdateTac kn ->
-    Tacenv.redefine_ltac local kn tac;
+    Tacenv.redefine_ltac local kn tac ?deprecation;
     let name = Tacenv.shortest_qualid_of_tactic kn in
     Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
   in
@@ -658,7 +660,7 @@ let lift_constr_tac_to_ml_tac vars tac =
   end in
   tac
 
-let tactic_extend plugin_name tacname ~level sign =
+let tactic_extend plugin_name tacname ~level ?deprecation sign =
   let open Tacexpr in
   let ml_tactic_name =
     { mltac_tactic = tacname;
@@ -687,10 +689,10 @@ let tactic_extend plugin_name tacname ~level sign =
       This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
     let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
     let id = Names.Id.of_string name in
-    let obj () = Tacenv.register_ltac true false id body in
+    let obj () = Tacenv.register_ltac true false id body ?deprecation in
     let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
     Mltop.declare_cache_obj obj plugin_name
   | _ ->
-  let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in
+  let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in
   Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
   Mltop.declare_cache_obj obj plugin_name
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index f873631ff..138a584e0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,10 +12,12 @@
 
 open Vernacexpr
 open Tacexpr
+open Vernacinterp
 
 (** {5 Tactic Definitions} *)
 
-val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
+val register_ltac : locality_flag -> ?deprecation:deprecation ->
+  Tacexpr.tacdef_body list -> unit
 (** Adds new Ltac definitions to the environment. *)
 
 (** {5 Tactic Notations} *)
@@ -34,8 +36,8 @@ type argument = Genarg.ArgT.any Extend.user_symbol
     leaves. *)
 
 val add_tactic_notation :
-  locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list ->
-  raw_tactic_expr -> unit
+  locality_flag -> int -> ?deprecation:deprecation -> raw_argument
+  grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit
 (** [add_tactic_notation local level prods expr] adds a tactic notation in the
     environment at level [level] with locality [local] made of the grammar
     productions [prods] and returning the body [expr] *)
@@ -47,7 +49,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -
     to finding an argument by name (as in {!Genarg}) if there is none
     matching. *)
 
-val add_ml_tactic_notation : ml_tactic_name -> level:int ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation ->
   argument grammar_tactic_prod_item_expr list list -> unit
 (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
     ML-side macro. *)
@@ -78,4 +80,5 @@ type _ ty_sig =
 
 type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
-val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit
+val tactic_extend : string -> string -> level:Int.t ->
+  ?deprecation:deprecation -> ty_ml list -> unit
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index d5ab2d690..0bb9ccb1d 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -52,7 +52,11 @@ let shortest_qualid_of_tactic kn =
 (** Tactic notations (TacAlias) *)
 
 type alias = KerName.t
-type alias_tactic = Id.t list * glob_tactic_expr
+type alias_tactic =
+  { alias_args: Id.t list;
+    alias_body: glob_tactic_expr;
+    alias_deprecation: Vernacinterp.deprecation option;
+  }
 
 let alias_map = Summary.ref ~name:"tactic-alias"
   (KNmap.empty : alias_tactic KNmap.t)
@@ -118,6 +122,7 @@ type ltac_entry = {
   tac_for_ml : bool;
   tac_body : glob_tactic_expr;
   tac_redef : ModPath.t list;
+  tac_deprecation : Vernacinterp.deprecation option
 }
 
 let mactab =
@@ -130,8 +135,12 @@ let interp_ltac r = (KNmap.find r !mactab).tac_body
 
 let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml
 
-let add kn b t =
-  let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in
+let add ~deprecation kn b t =
+  let entry = { tac_for_ml = b;
+                tac_body = t;
+                tac_redef = [];
+                tac_deprecation = deprecation;
+              } in
   mactab := KNmap.add kn entry !mactab
 
 let replace kn path t =
@@ -139,34 +148,38 @@ let replace kn path t =
   let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
   mactab := KNmap.modify kn entry !mactab
 
-let load_md i ((sp, kn), (local, id, b, t)) = match id with
+let tac_deprecation kn =
+  try (KNmap.find kn !mactab).tac_deprecation with Not_found -> None
+
+let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
 | None ->
   let () = if not local then push_tactic (Until i) sp kn in
-  add kn b t
+  add ~deprecation kn b t
 | Some kn0 -> replace kn0 kn t
 
-let open_md i ((sp, kn), (local, id, b, t)) = match id with
+let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
 | None ->
   let () = if not local then push_tactic (Exactly i) sp kn in
-  add kn b t
+  add ~deprecation kn b t
 | Some kn0 -> replace kn0 kn t
 
-let cache_md ((sp, kn), (local, id ,b, t)) = match id with
+let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with
 | None ->
   let () = push_tactic (Until 1) sp kn in
-  add kn b t
+  add ~deprecation kn b t
 | Some kn0 -> replace kn0 kn t
 
 let subst_kind subst id = match id with
 | None -> None
 | Some kn -> Some (Mod_subst.subst_kn subst kn)
 
-let subst_md (subst, (local, id, b, t)) =
-  (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t)
+let subst_md (subst, (local, id, b, t, deprecation)) =
+  (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t, deprecation)
 
-let classify_md (local, _, _, _ as o) = Substitute o
+let classify_md (local, _, _, _, _ as o) = Substitute o
 
-let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
+let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
+           Vernacinterp.deprecation option -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
@@ -174,8 +187,8 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
      subst_function = subst_md;
      classify_function = classify_md}
 
-let register_ltac for_ml local id tac =
-  ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac)))
+let register_ltac for_ml local ?deprecation id tac =
+  ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac, deprecation)))
 
-let redefine_ltac local kn tac =
-  Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac))
+let redefine_ltac local ?deprecation kn tac =
+  Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac, deprecation))
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 3af2f2a46..7143f5185 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,6 +12,7 @@ open Names
 open Libnames
 open Tacexpr
 open Geninterp
+open Vernacinterp
 
 (** This module centralizes the various ways of registering tactics. *)
 
@@ -29,7 +30,11 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid
 type alias = KerName.t
 (** Type of tactic alias, used in the [TacAlias] node. *)
 
-type alias_tactic = Id.t list * glob_tactic_expr
+type alias_tactic =
+  { alias_args: Id.t list;
+    alias_body: glob_tactic_expr;
+    alias_deprecation: Vernacinterp.deprecation option;
+  }
 (** Contents of a tactic notation *)
 
 val register_alias : alias -> alias_tactic -> unit
@@ -43,7 +48,8 @@ val check_alias : alias -> bool
 
 (** {5 Coq tactic definitions} *)
 
-val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
+val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t ->
+  glob_tactic_expr -> unit
 (** Register a new Ltac with the given name and body.
 
     The first boolean indicates whether this is done from ML side, rather than
@@ -51,7 +57,8 @@ val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
     definition. It also puts the Ltac name in the nametab, so that it can be
     used unqualified. *)
 
-val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit
+val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t ->
+  glob_tactic_expr -> unit
 (** Replace a Ltac with the given name and body. If the boolean flag is set
     to true, then this is a local redefinition. *)
 
@@ -61,6 +68,9 @@ val interp_ltac : KerName.t -> glob_tactic_expr
 val is_ltac_for_ml_tactic : KerName.t -> bool
 (** Whether the tactic is defined from ML-side *)
 
+val tac_deprecation : KerName.t -> deprecation option
+(** The tactic deprecation notice, if any *)
+
 type ltac_entry = {
   tac_for_ml : bool;
   (** Whether the tactic is defined from ML-side *)
@@ -68,6 +78,8 @@ type ltac_entry = {
   (** The current body of the tactic *)
   tac_redef : ModPath.t list;
   (** List of modules redefining the tactic in reverse chronological order *)
+  tac_deprecation : deprecation option;
+  (** Deprecation notice to be printed when the tactic is used *)
 }
 
 val ltac_entries : unit -> ltac_entry KNmap.t
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 06d2711ad..59b748e25 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -398,5 +398,5 @@ type ltac_call_kind =
 type ltac_trace = ltac_call_kind Loc.located list
 
 type tacdef_body =
-  | TacticDefinition of lident * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
-  | TacticRedefinition of qualid * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
+  | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+  | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 71e1edfd7..3a0badb28 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -398,5 +398,5 @@ type ltac_call_kind =
 type ltac_trace = ltac_call_kind Loc.located list
 
 type tacdef_body =
-  | TacticDefinition of lident * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
-  | TacticRedefinition of qualid * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
+  | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+  | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 481fc30df..144480062 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -117,9 +117,26 @@ let intern_constr_reference strict ist qid =
 
 (* Internalize an isolated reference in position of tactic *)
 
+let warn_deprecated_tactic =
+  CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated"
+    (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++
+      strbrk " is deprecated" ++
+      pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+
+let warn_deprecated_alias =
+  CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated"
+    (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++
+      strbrk " is deprecated since" ++
+      pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+
 let intern_isolated_global_tactic_reference qid =
   let loc = qid.CAst.loc in
-  TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
+  let kn = Tacenv.locate_tactic qid in
+  Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
+    Tacenv.tac_deprecation kn;
+  TacCall (Loc.tag ?loc (ArgArg (loc,kn),[]))
 
 let intern_isolated_tactic_reference strict ist qid =
   (* An ltac reference *)
@@ -137,7 +154,11 @@ let intern_isolated_tactic_reference strict ist qid =
 (* Internalize an applied tactic reference *)
 
 let intern_applied_global_tactic_reference qid =
-  ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid)
+  let loc = qid.CAst.loc in
+  let kn = Tacenv.locate_tactic qid in
+  Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
+    Tacenv.tac_deprecation kn;
+  ArgArg (loc,kn)
 
 let intern_applied_tactic_reference ist qid =
   (* An ltac reference *)
@@ -643,6 +664,8 @@ and intern_tactic_seq onlytac ist = function
 
   (* For extensions *)
   | TacAlias (loc,(s,l)) ->
+      let alias = Tacenv.interp_alias s in
+      Option.iter (fun o -> warn_deprecated_alias ?loc (s,o)) @@ alias.Tacenv.alias_deprecation;
       let l = List.map (intern_tacarg !strict_check false ist) l in
       ist.ltacvars, TacAlias (Loc.tag ?loc (s,l))
   | TacML (loc,(opn,l)) ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d9ac96d89..77b5b06d4 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1125,17 +1125,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
   | TacAlias (loc,(s,l)) ->
-      let (ids, body) = Tacenv.interp_alias s in
+      let alias = Tacenv.interp_alias s in
       let (>>=) = Ftactic.bind in
       let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
       let tac l =
         let addvar x v accu = Id.Map.add x v accu in
-        let lfun = List.fold_right2 addvar ids l ist.lfun in
+        let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
         Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
         let ist = {
           lfun = lfun;
           extra = TacStore.set ist.extra f_trace trace; } in
-        val_interp ist body >>= fun v ->
+        val_interp ist alias.Tacenv.alias_body >>= fun v ->
         Ftactic.lift (tactic_of_value ist v)
       in
       let tac =
@@ -1147,7 +1147,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
          some more elaborate solution will have to be used. *)
       in
       let tac =
-        let len1 = List.length ids in
+        let len1 = List.length alias.Tacenv.alias_args in
         let len2 = List.length l in
         if len1 = len2 then tac
         else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
diff --git a/plugins/micromega/Fourier.v b/plugins/micromega/Fourier.v
new file mode 100644
index 000000000..0153de1da
--- /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 000000000..b62153dee
--- /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/mutils.mli b/plugins/micromega/mutils.mli
index 7b7a090de..094429ea1 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