Improved robustness of micromega parser. Proof search of Micromega test-suites is now bounded -- ensure termination

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11200 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 152 insertions, 207 deletions

diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml
index 3d6d5bcfa..02ff61a19 100644
--- a/contrib/micromega/coq_micromega.ml
+++ b/contrib/micromega/coq_micromega.ml
@@ -106,6 +106,7 @@ struct
      ["Coq" ; "micromega" ; "EnvRing"];
      ["Coq";"QArith"; "QArith_base"];
      ["Coq";"Reals" ; "Rdefinitions"];
+     ["Coq";"Reals" ; "Rpow_def"];
      ["LRing_normalise"]]
    
  let constant = gen_constant_in_modules "ZMicromega" coq_modules
@@ -163,6 +164,9 @@ struct
 
 
  let coq_Qmake = lazy (constant "Qmake")
+ let coq_R0    = lazy (constant "R0")
+ let coq_R1    = lazy (constant "R1")
+
 
  let coq_proofTerm = lazy (constant "ProofTerm")
  let coq_ratProof = lazy (constant "RatProof")
@@ -179,10 +183,36 @@ struct
  let coq_Zminus = lazy (constant "Zminus")
  let coq_Zopp = lazy (constant "Zopp")
  let coq_Zmult = lazy (constant "Zmult")
+ let coq_Zpower = lazy (constant "Zpower")
  let coq_N_of_Z = lazy 
   (gen_constant_in_modules "ZArithRing" 
     [["Coq";"setoid_ring";"ZArithRing"]] "N_of_Z")
 
+ let coq_Qgt = lazy (constant "Qgt")
+ let coq_Qge = lazy (constant "Qge")
+ let coq_Qle = lazy (constant "Qle")
+ let coq_Qlt = lazy (constant "Qlt")
+ let coq_Qeq = lazy (constant "Qeq")
+
+
+ let coq_Qplus = lazy (constant "Qplus")
+ let coq_Qminus = lazy (constant "Qminus")
+ let coq_Qopp = lazy (constant "Qopp")
+ let coq_Qmult = lazy (constant "Qmult")
+ let coq_Qpower = lazy (constant "Qpower")
+
+
+ let coq_Rgt = lazy (constant "Rgt")
+ let coq_Rge = lazy (constant "Rge")
+ let coq_Rle = lazy (constant "Rle")
+ let coq_Rlt = lazy (constant "Rlt")
+
+ let coq_Rplus = lazy (constant "Rplus")
+ let coq_Rminus = lazy (constant "Rminus")
+ let coq_Ropp = lazy (constant "Ropp")
+ let coq_Rmult = lazy (constant "Rmult")
+ let coq_Rpower = lazy (constant "pow")
+
 
  let coq_PEX = lazy (constant "PEX" )
  let coq_PEc = lazy (constant"PEc")
@@ -225,6 +255,7 @@ struct
   (gen_constant_in_modules "RingMicromega" 
     [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] "Formula")
 
+
  type parse_error  = 
    | Ukn 
    | BadStr of string 
@@ -347,16 +378,11 @@ let dump_q q =
 
 let parse_q term =  
  match Term.kind_of_term term with
-  | Term.App(c, args) -> 
-     (
-      match Term.kind_of_term c with
-	Term.Construct((n,j),i) -> 
-      if Names.string_of_kn n  = "Coq.QArith.QArith_base#<>#Q"
-      then {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
+  | Term.App(c, args) -> if c = Lazy.force coq_Qmake then
+	{Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
       else raise ParseError
-       |  _ -> raise ParseError
-     )
-  |   _ -> raise ParseError
+  |  _ -> raise ParseError
+
   
  let rec parse_list parse_elt term = 
   let (i,c) = get_left_construct term in
@@ -466,19 +492,6 @@ let parse_q term =
    pp_cone o e
 
 
-
-
- let rec parse_op term = 
-  let (i,c) = get_left_construct term in
-   match i with
-    | 1 -> Mc.OpEq
-    | 2 -> Mc.OpLe
-    | 3 -> Mc.OpGe
-    | 4 -> Mc.OpGt
-    | 5 -> Mc.OpLt
-    | i -> raise ParseError
-
-
  let rec dump_op = function
   | Mc.OpEq-> Lazy.force coq_OpEq
   | Mc.OpNEq-> Lazy.force coq_OpNEq
@@ -510,68 +523,52 @@ let parse_q term =
 		dump_op o ; 
 		dump_expr typ dump_constant e2|])
 
+ let assoc_const x l = 
+  try 
+  snd (List.find (fun (x',y) -> x = Lazy.force x') l)
+  with
+    Not_found -> raise ParseError
+
+ let zop_table = [ 
+  coq_Zgt, Mc.OpGt ; 
+  coq_Zge, Mc.OpGe ;
+  coq_Zlt, Mc.OpLt ;
+  coq_Zle, Mc.OpLe ]
+
+ let rop_table = [ 
+  coq_Rgt, Mc.OpGt ; 
+  coq_Rge, Mc.OpGe ;
+  coq_Rlt, Mc.OpLt ;
+  coq_Rle, Mc.OpLe ]
+
+ let qop_table = [ 
+  coq_Qlt, Mc.OpLt ;
+  coq_Qle, Mc.OpLe ;
+  coq_Qeq, Mc.OpEq
+ ]
 
 
  let parse_zop (op,args) =
   match kind_of_term op with
-   | Const x -> 
-      (match Names.string_of_con x with
-       | "Coq.ZArith.BinInt#<>#Zgt" -> (Mc.OpGt, args.(0), args.(1))
-       | "Coq.ZArith.BinInt#<>#Zge" -> (Mc.OpGe, args.(0), args.(1))
-       | "Coq.ZArith.BinInt#<>#Zlt" -> (Mc.OpLt, args.(0), args.(1))
-       | "Coq.ZArith.BinInt#<>#Zle" -> (Mc.OpLe, args.(0), args.(1))
-       (*| "Coq.Init.Logic#<>#not"    -> Mc.OpNEq  (* for backward compat *)*)
-       |   s -> raise ParseError
-      )
+   | Const x -> (assoc_const op zop_table, args.(0) , args.(1))
    |  Ind(n,0) -> 
-       (match Names.string_of_kn n with
-	| "Coq.Init.Logic#<>#eq" -> 
-	   if args.(0) <> Lazy.force coq_Z
-	   then raise ParseError
-	   else (Mc.OpEq, args.(1), args.(2))
-	|  _ -> raise ParseError)
+       if op = Lazy.force coq_Eq &&   args.(0) = Lazy.force coq_Z
+       then (Mc.OpEq, args.(1), args.(2))
+       else raise ParseError
    |   _ -> failwith "parse_zop"
 
 
  let parse_rop (op,args) =
-  try 
    match kind_of_term op with
-    | Const x -> 
-       (match Names.string_of_con x with
-	| "Coq.Reals.Rdefinitions#<>#Rgt" -> (Mc.OpGt, args.(0), args.(1))
-	| "Coq.Reals.Rdefinitions#<>#Rge" -> (Mc.OpGe, args.(0), args.(1))
-	| "Coq.Reals.Rdefinitions#<>#Rlt" -> (Mc.OpLt, args.(0), args.(1))
-	| "Coq.Reals.Rdefinitions#<>#Rle" -> (Mc.OpLe, args.(0), args.(1))
-	   (*| "Coq.Init.Logic#<>#not"-> Mc.OpNEq  (* for backward compat *)*)
-       |   s -> raise ParseError
-       )
+    | Const x -> (assoc_const op rop_table, args.(0) , args.(1))
     |  Ind(n,0) -> 
-	(match Names.string_of_kn n with
-	 | "Coq.Init.Logic#<>#eq" -> 
-	    (*   if args.(0) <> Lazy.force coq_R
-		 then raise ParseError
-		 else*) (Mc.OpEq, args.(1), args.(2))
-	 |  _ -> raise ParseError)
-    |   _ -> failwith "parse_rop"
-  with x -> 
-   (Pp.pp (Pp.str "parse_rop failure ") ; 
-    Pp.pp (Printer.prterm op) ; Pp.pp_flush ()) 
-   ; raise x
-
+       if op = Lazy.force coq_Eq &&   args.(0) = Lazy.force coq_R
+       then (Mc.OpEq, args.(1), args.(2))
+       else raise ParseError
+   |   _ -> failwith "parse_zop"
 
  let parse_qop (op,args) =
-  (
-   (match kind_of_term op with
-   | Const x -> 
-      (match Names.string_of_con x with
-       | "Coq.QArith.QArith_base#<>#Qgt" -> Mc.OpGt
-       | "Coq.QArith.QArith_base#<>#Qge" -> Mc.OpGe
-       | "Coq.QArith.QArith_base#<>#Qlt" -> Mc.OpLt
-       | "Coq.QArith.QArith_base#<>#Qle" -> Mc.OpLe
-       | "Coq.QArith.QArith_base#<>#Qeq" -> Mc.OpEq
-       |   s -> raise ParseError
-      )
-   |   _ -> failwith "parse_zop") , args.(0) , args.(1))
+   (assoc_const op qop_table, args.(0) , args.(1))
 
 
  module Env =
@@ -612,6 +609,14 @@ let parse_q term =
    | Ukn of string
 
 
+ let assoc_ops x l = 
+  try 
+    snd (List.find (fun (x',y) -> x = Lazy.force x') l)
+  with
+    Not_found -> Ukn "Oups"
+
+
+
  let parse_expr parse_constant parse_exp ops_spec env term = 
  if debug 
  then (Pp.pp (Pp.str "parse_expr: ");   
@@ -634,7 +639,7 @@ let parse_q term =
 	(
 	 match kind_of_term t with
 	  | Const c -> 
-	     ( match ops_spec (Names.string_of_con c) with
+	     ( match assoc_ops t ops_spec  with
 	      | Binop f -> combine env f (args.(0),args.(1))
 	      | Opp     -> let (expr,env) = parse_expr env args.(0) in
 			    (Mc.PEopp expr, env)
@@ -653,29 +658,29 @@ let parse_q term =
    parse_expr env term
     
 
-let zop_spec = function
- | "Coq.ZArith.BinInt#<>#Zplus"    -> Binop (fun x y -> Mc.PEadd(x,y))
- | "Coq.ZArith.BinInt#<>#Zminus"   -> Binop (fun x y -> Mc.PEsub(x,y)) 
- | "Coq.ZArith.BinInt#<>#Zmult"    -> Binop  (fun x y -> Mc.PEmul (x,y))
-  | "Coq.ZArith.BinInt#<>#Zopp"     ->  Opp
-  | "Coq.ZArith.Zpow_def#<>#Zpower" -> Power
-  |  s                                   -> Ukn s
+ let zop_spec = 
+   [ 
+     coq_Zplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+     coq_Zminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+     coq_Zmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ; 
+     coq_Zopp   , Opp ; 
+     coq_Zpower , Power]
 
-let qop_spec = function
- | "Coq.QArith.QArith_base#<>#Qplus"    -> Binop (fun x y -> Mc.PEadd(x,y))
- | "Coq.QArith.QArith_base#<>#Qminus"   -> Binop (fun x y -> Mc.PEsub(x,y)) 
- | "Coq.QArith.QArith_base#<>#Qmult"    -> Binop  (fun x y -> Mc.PEmul (x,y)) 
-  | "Coq.QArith.QArith_base#<>#Qopp"     ->  Opp
-  | "Coq.QArith.QArith_base#<>#Qpower" -> Power
-  |  s                                   -> Ukn s
+let qop_spec = 
+  [
+     coq_Qplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+     coq_Qminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+     coq_Qmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ; 
+     coq_Qopp   , Opp ; 
+     coq_Qpower , Power]
 
-let rop_spec = function
- | "Coq.Reals.Rdefinitions#<>#Rplus"    -> Binop (fun x y -> Mc.PEadd(x,y))
- | "Coq.Reals.Rdefinitions#<>#Rminus"   -> Binop (fun x y -> Mc.PEsub(x,y)) 
- | "Coq.Reals.Rdefinitions#<>#Rmult"    -> Binop  (fun x y -> Mc.PEmul (x,y))
- | "Coq.Reals.Rdefinitions#<>#Ropp"     -> Opp
- | "Coq.Reals.Rpow_def#<>#pow"          -> Power
- |  s                                        -> Ukn s
+let rop_spec = 
+  [
+     coq_Rplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+     coq_Rminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+     coq_Rmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ; 
+     coq_Ropp   , Opp ; 
+     coq_Rpower , Power]
 
 
 
@@ -691,12 +696,12 @@ let rconstant term =
        Pp.pp (Pp.str "rconstant: ");
        Pp.pp (Printer.prterm  term); Pp.pp_flush ());
  match Term.kind_of_term term with
-  | Const x ->        
-     (match Names.string_of_con x with
-      | "Coq.Reals.Rdefinitions#<>#R0" -> Mc.Z0
-      | "Coq.Reals.Rdefinitions#<>#R1" -> Mc.Zpos Mc.XH
-      | _   -> raise ParseError
-     )
+  | Const x ->  
+      if term = Lazy.force coq_R0
+      then Mc.Z0
+      else if term = Lazy.force coq_R1
+      then Mc.Zpos Mc.XH
+      else raise ParseError
   |  _ -> raise ParseError
 
 
@@ -731,23 +736,6 @@ let parse_rexpr =
   
  (* generic parsing of arithmetic expressions *)
   
- let rec parse_conj parse_arith env term = 
-  match kind_of_term term with
-   | App(l,rst) -> 
-      (match kind_of_term l with
-       | Ind (n,_) -> 
-	  ( match Names.string_of_kn n with
-	   | "Coq.Init.Logic#<>#and" -> 
-	      let (e1,env) = parse_arith env rst.(0) in
-	      let (e2,env) = parse_conj parse_arith env rst.(1) in
-	       (Mc.Cons(e1,e2),env)
-	   |   _ -> (* This might be an equality *) 
-		let (e,env) = parse_arith env term in
-		 (Mc.Cons(e,Mc.Nil),env))
-       |  _ -> (* This is an arithmetic expression *)
-	   let (e,env) = parse_arith env term in
-	    (Mc.Cons(e,Mc.Nil),env))
-   |  _ -> failwith "parse_conj(2)"
 
 
 
@@ -850,46 +838,6 @@ let parse_rexpr =
    xdump f
     
 
- (* Backward compat *)
-
- let rec parse_concl parse_arith env term =
-  match kind_of_term term with
-   | Prod(_,expr,rst) -> (* a -> b *)
-      let (lhs,rhs,env) = parse_concl parse_arith env rst in
-      let (e,env) = parse_arith env expr in
-       (Mc.Cons(e,lhs),rhs,env)
-   | App(_,_) -> 
-      let (conj, env) = parse_conj parse_arith env term in
-       (Mc.Nil,conj,env)
-   |  Ind(n,_) -> 
-       (match (Names.string_of_kn n) with
-	| "Coq.Init.Logic#<>#False" -> (Mc.Nil,Mc.Nil,env)
-	|    s                           -> 
-	      print_string s ; flush stdout;
-	      failwith "parse_concl")
-   |  _ -> failwith "parse_concl"
-
-
- let rec parse_hyps parse_arith env goal_hyps hyps = 
-  match hyps with
-   | [] -> ([],goal_hyps,env)
-   | (i,t)::l -> 
-      let (li,lt,env) = parse_hyps parse_arith env goal_hyps l in
-       try 
-	let (c,env) = parse_arith env  t in
-	 (i::li, Mc.Cons(c,lt), env)
-       with  x -> 
-	(*(if debug then Printf.printf "parse_arith : %s\n" x);*)
-	(li,lt,env)
-
-
- let parse_goal parse_arith env hyps term = 
-  try
-   let (lhs,rhs,env) = parse_concl parse_arith env term in
-   let (li,lt,env) = parse_hyps parse_arith env lhs hyps in
-    (li,lt,rhs,env)
-  with Failure x -> raise ParseError
-   (* backward compat *)
 
 
  (* ! reverse the list of bindings *)
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index 11e3e8cce..234d51134 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -17,11 +17,11 @@ Load the {\tt Psatz} module ({\tt Require Psatz}.).  This module defines the tac
   \begin{itemize}
   \item The {\tt psatzl} tactic solves linear goals using an embedded (naive) linear programming prover \emph{i.e.},
     fourier elimination.
-  \item The {\tt psatz} tactic solves polynomial goals using an external prover {\tt cspd}\footnote{Source and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating 
+  \item The {\tt psatz} tactic solves polynomial goals using John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Source and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating 
     a \emph{proof cache} thus allowing to rerun scripts even without {\tt csdp}. 
   \item The {\tt lia} (linear integer arithmetic) tactic is specialised to solve linear goals over $\mathbb{Z}$.
     It extends {\tt psatzl Z} and exploits the discreetness of $\mathbb{Z}$.
-  \item The {\tt sos} tactic is another driver to the {\tt csdp} prover.  In theory, it is less general than
+  \item The {\tt sos} tactic is another Hol light driver to the {\tt csdp} prover.  In theory, it is less general than
     {\tt psatz}. In practice, even when {\tt psatz} fails, it can be worth a try -- see
     Section~\ref{sec:psatz-back} for details.
   \end{itemize}
diff --git a/test-suite/micromega/bertot.v b/test-suite/micromega/bertot.v
index 8e9c0c6de..bcf222f92 100644
--- a/test-suite/micromega/bertot.v
+++ b/test-suite/micromega/bertot.v
@@ -17,6 +17,6 @@ Goal (forall x y n,
   (x < n /\ x <= n /\ 2 * y = x * (x+1) -> x + 1 <= n /\ 2 *(x+1+y) = (x+1)*(x+2))).
 Proof.
   intros.
-  psatz Z.
+  psatz Z 3.
 Qed.
 
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index 23bea439a..905b9a938 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -28,14 +28,14 @@ Qed.
 Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
 Proof.
   intros. 
-  psatz Z. 
+  psatz Z 2. 
 Qed.
 
 
 Lemma Zdiscr: forall a b c x, 
   a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 4.
 Qed.
 
 
@@ -51,13 +51,13 @@ Qed.
 Lemma mplus_minus : forall x y, 
   x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma pol3: forall x y, 0 <= x + y ->  
   x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 4.
 Qed.
 
 
@@ -96,7 +96,7 @@ Proof.
   generalize (H8 _ _ _ (conj H5 H4)).
   generalize (H10 _ _ _ (conj H5 H4)).
   generalize rho_ge.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 (* Rule of signs *)
@@ -104,55 +104,55 @@ Qed.
 Lemma sign_pos_pos: forall x y,
   x > 0 -> y > 0 -> x*y > 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_pos_zero: forall x y,
   x > 0 -> y = 0 -> x*y = 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_pos_neg: forall x y,
   x > 0 -> y < 0 -> x*y < 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_zer_pos: forall x y,
   x = 0 -> y > 0 -> x*y = 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_zero_zero: forall x y,
   x = 0 -> y = 0 -> x*y = 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_zero_neg: forall x y,
   x = 0 -> y < 0 -> x*y = 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_neg_pos: forall x y,
   x < 0 -> y > 0 -> x*y < 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_neg_zero: forall x y,
   x < 0 -> y = 0 -> x*y = 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_neg_neg: forall x y,
   x < 0 -> y < 0 -> x*y > 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 
@@ -167,20 +167,20 @@ Qed.
 Lemma product : forall x y, x >= 0 -> y >= 0 -> x * y >= 0.
 Proof.
   intros.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 
 Lemma product_strict : forall x y, x > 0 -> y > 0 -> x * y > 0.
 Proof.
   intros.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 
 Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 ->  False.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 2.
 Qed.
 
 (* Found in Parrilo's talk *)
@@ -188,7 +188,7 @@ Qed.
 Lemma parrilo_ex : forall x y, x - y^2 + 3 >= 0 -> y + x^2 + 2 = 0 -> False.
 Proof.
   intros.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 (* from hol_light/Examples/sos.ml *)
@@ -198,26 +198,26 @@ Lemma hol_light1 : forall a1 a2 b1 b2,
    (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) -> 
    (a1 * b1 + a2 * b2 = 0) -> a1 * a2 - b1 * b2 >= 0.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 4.
 Qed.
 
 
 Lemma hol_light2 : forall x a,
         3 * x + 7 * a < 4 -> 3 < 2 * x -> a < 0.
 Proof.
- intros ; psatz Z.
+ intros ; psatz Z 2.
 Qed.
 
 Lemma hol_light3 : forall b a c x,
   b ^ 2 < 4 * a * c -> (a * x ^2  + b * x + c = 0) -> False.
 Proof.
-intros ; psatz Z.
+intros ; psatz Z 4.
 Qed.
 
 Lemma hol_light4 : forall a c b x,
   a * x ^ 2 + b * x + c = 0 -> b ^ 2 >= 4 * a * c.
 Proof.
-intros ; psatz Z.
+intros ; psatz Z 4.
 Qed.
 
 Lemma hol_light5 : forall x y,
@@ -227,7 +227,7 @@ Lemma hol_light5 : forall x y,
       x ^ 2 + (y - 1) ^ 2 < 1 \/
       (x - 1) ^ 2 + (y - 1) ^ 2 < 1.
 Proof.
-intros; psatz Z.
+intros; psatz Z 3.
 Qed.
 
 
@@ -236,32 +236,32 @@ Lemma hol_light7 : forall x y z,
  0<= x /\ 0 <= y /\ 0 <= z /\ x + y + z <= 3
   -> x * y + x * z + y * z >= 3 * x * y * z.
 Proof.
-intros ; psatz Z.
+intros ; psatz Z 3.
 Qed.
 
 Lemma hol_light8 : forall x y z,
  x ^ 2 + y ^ 2 + z ^ 2 = 1 -> (x + y + z) ^ 2 <= 3.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 2.
 Qed.
 
 Lemma hol_light9 : forall w x y z,
  w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1
   -> (w + x + y + z) ^ 2 <= 4.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma hol_light10 : forall x y,
  x >= 1 /\ y >= 1 -> x * y >= x + y - 1.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 2.
 Qed.
 
 Lemma hol_light11 : forall x y,
  x > 1 /\ y > 1 -> x * y > x + y - 1.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 2.
 Qed.
 
 
@@ -273,14 +273,14 @@ Lemma hol_light12: forall x y z,
 Proof.
   intros x y z ; set (e:= (125841 / 50000)).
   compute in e.
-  unfold e ; intros ; psatz Z.
+  unfold e ; intros ; psatz Z 2.
 Qed.
 
 Lemma hol_light14 : forall x y z,
  2 <= x /\ x <= 4 /\ 2 <= y /\ y <= 4 /\ 2 <= z /\ z <= 4
   -> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z).
 Proof.
-  intros ;psatz Z.
+  intros ;psatz Z 2.
 Qed.
 
 (* ------------------------------------------------------------------------- *)
@@ -291,20 +291,20 @@ Lemma hol_light16 : forall x y,
   0 <= x /\ 0 <= y /\ (x * y = 1)
    -> x + y <= x ^ 2 + y ^ 2.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 2.
 Qed.
 
 Lemma hol_light17 : forall x y,
   0 <= x /\ 0 <= y /\ (x * y = 1)
    -> x * y * (x + y) <= x ^ 2 + y ^ 2.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 3.
 Qed.
 
 Lemma hol_light18 : forall x y,
   0 <= x /\ 0 <= y -> x * y * (x + y) ^ 2 <= (x ^ 2 + y ^ 2) ^ 2.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 4.
 Qed.
 
 (* ------------------------------------------------------------------------- *)
@@ -319,7 +319,7 @@ Qed.
 Lemma hol_light22 : forall n, n >= 0 -> n <= n * n.
 Proof.
   intros.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 
@@ -328,7 +328,7 @@ Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0
                 -> (x1 + y1 = x2 + y2).
 Proof.
   intros.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0.
@@ -342,5 +342,5 @@ Lemma motzkin : forall x y, (x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2)  >= 0.
 Proof.
   intros.
   generalize (motzkin' x y).
-  psatz Z.
+  psatz Z 8.
 Qed.
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index cdecebfcd..8a349a1d9 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -17,6 +17,9 @@ Proof.
   psatzl Q.
 Qed.
 
+
+
+
 (* Other (simple) examples *)
 Open Scope Q_scope.
 
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 5738ebbff..1de1955db 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -12,7 +12,7 @@ Require Import Ring_normalize.
 
 Open Scope R_scope.
 
-Lemma plus_minus : forall x y, 
+Lemma yplus_minus : forall x y, 
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
@@ -74,10 +74,4 @@ Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
 intros; split_Rabs; psatzl R.
-Qed.
- 
-Lemma l2 :
- forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1.
-intros.
-split_Rabs; psatzl R.
-Qed.
+Qed.
\ No newline at end of file
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 5594afbb9..b78bba25c 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -11,7 +11,7 @@ Open Scope Z_scope.
 
 Lemma Zabs_square : forall x,  (Zabs  x)^2 = x^2.
 Proof.
- intros ; case (Zabs_dec x) ; intros ; psatz Z.
+ intros ; case (Zabs_dec x) ; intros ; psatz Z 2.
 Qed.
 Hint Resolve Zabs_pos Zabs_square.
 
@@ -21,11 +21,11 @@ intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p).
 assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2
          /\ Zabs p^2 = p^2) by auto.
 assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by 
-  (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z).
+  (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2).
 generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
 intros n IHn p [Hn [Hp Heq]].
-assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; psatz Z).
-assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by psatz Z.
+assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; psatz Z 2).
+assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by psatz Z 2.
 apply (IHn (2*p-n) Hzwf (n-p) Hdecr).
 Qed.