micromega : more robust generation of proof terms

- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
  (This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)

3 files changed, 52 insertions, 3 deletions

diff --git a/test-suite/micromega/bertot.v b/test-suite/micromega/bertot.v
index bcf222f92..29171aed9 100644
--- a/test-suite/micromega/bertot.v
+++ b/test-suite/micromega/bertot.v
@@ -11,6 +11,8 @@ Require Import Psatz.
 
 Open Scope Z_scope.
 
+
+
 Goal (forall x y n,
   ( ~ x < n /\ x <= n /\ 2 * y = x*(x+1) -> 2 * y = n*(n+1))
   /\
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 89c08c770..12f72a580 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -11,6 +11,12 @@ Require Import Reals.
 
 Open Scope R_scope.
 
+
+Lemma cst_test : 5^5 = 5 * 5 * 5 *5 *5.
+Proof.
+  lra.
+Qed.
+
 Lemma yplus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
@@ -73,4 +79,5 @@ Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
 intros; split_Rabs; lra.
-Qed.
\ No newline at end of file
+Qed.
+
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 1f148becc..3f4c2407d 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -8,9 +8,10 @@ Proof.
   lia.
 Qed.
 
+
 Lemma two_x_y_eq_1 : forall x y, 2 * x + 2 * y = 1 -> False.
 Proof.
-  intros.
+  intros. 
   lia.
 Qed.
 
@@ -20,6 +21,12 @@ Proof.
   lia.
 Qed.
 
+Lemma unused : forall x y, y >= 0 /\ x = 1 -> x = 1.
+Proof.
+  intros x y.
+  lia.
+Qed.
+
 Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 ->  -10 <= 7 * x - 9 * y <= 4 -> False.
 Proof.
   intros ; intuition auto.
@@ -42,4 +49,37 @@ Proof.
   Unshelve.
   exact Z0.
 Qed.
-  
\ No newline at end of file
+
+Lemma unused_concl : forall x,
+    False -> x > 0 -> x < 0.
+Proof.
+  intro.
+  lia.
+Qed.
+
+Lemma unused_concl_match : forall (x:Z),
+    False -> match x with
+             | Z0 => True
+             | _ => x = x
+             end.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Lemma fresh : forall (__arith : Prop),
+    __arith -> True.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Class Foo {x : Z} := { T : Type ; dec : T -> Z }.
+Goal forall bound {F : @Foo bound} (x y : T), 0 <= dec x < bound -> 0 <= dec y 
+< bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound.
+Proof.
+  intros.
+  lia.
+Qed.
+
+