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)

1 files changed, 42 insertions, 2 deletions

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.
+
+