7 files changed, 64 insertions, 32 deletions
diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v
index 75b2a56169..fbd9c8bcba 100644
--- a/test-suite/failure/Template.v
+++ b/test-suite/failure/Template.v
@@ -1,4 +1,4 @@
-(*
+
 Module TestUnsetTemplateCheck.
   Unset Template Check.
 
@@ -15,18 +15,14 @@ Module TestUnsetTemplateCheck.
   (* Can only succeed if no template check is performed *)
   Check myind True : Prop.
 
-  Print Assumptions myind.
-  (*
-  Axioms:
-  myind is template polymorphic on all its universe parameters.
-   *)
   About myind.
-(*
-myind : Type@{Top.60} -> Type@{Top.60}
 
-myind is assumed template universe polymorphic on Top.60
-Argument scope is [type_scope]
-Expands to: Inductive Top.TestUnsetTemplateCheck.myind
-*)
+  (* test discharge puts things in the right order (by using the
+     checker on the result) *)
+  Section S.
+
+    Variables (A:Type) (a:A).
+    Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B.
+  End S.
+
 End TestUnsetTemplateCheck.
-*)
diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out
new file mode 100644
index 0000000000..6bc04f1cef
--- /dev/null
+++ b/test-suite/output/QArithSyntax.out
@@ -0,0 +1,14 @@
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : 102e-1 = 102e-1
+     : 102e-1 = 102e-1
+eq_refl : 1020 = 1020
+     : 1020 = 1020
+eq_refl : 102 = 102
+     : 102 = 102
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : -1e-4 = -1e-4
+     : -1e-4 = -1e-4
+eq_refl : -50e-2 = -50e-2
+     : -50e-2 = -50e-2
diff --git a/test-suite/success/QArithSyntax.v b/test-suite/output/QArithSyntax.v
index 2f2ee0134a..2f2ee0134a 100644
--- a/test-suite/success/QArithSyntax.v
+++ b/test-suite/output/QArithSyntax.v
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index e6f7556d96..2d877bd813 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -2,3 +2,17 @@
      : R
 (-31)%R
      : R
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : 102e-1 = 102e-1
+     : 102e-1 = 102e-1
+eq_refl : 102e1 = 102e1
+     : 102e1 = 102e1
+eq_refl : 102 = 102
+     : 102 = 102
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : -1e-4 = -1e-4
+     : -1e-4 = -1e-4
+eq_refl : -50e-2 = -50e-2
+     : -50e-2 = -50e-2
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 44e8c7a50c..cb3bce70d4 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -1,3 +1,25 @@
 Require Import Reals.Rdefinitions.
 Check 32%R.
 Check (-31)%R.
+
+Open Scope R_scope.
+
+Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).
+Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)).
+Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)).
+Check (eq_refl : 1.02e+02 = IZR 102).
+Check (eq_refl : 10.2e-1 = 1.02).
+Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)).
+Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)).
+
+Require Import Reals.
+
+Goal 254e3 = 2540 * 10 ^ 2.
+ring.
+Qed.
+
+Require Import Psatz.
+
+Goal 254e3 = 2540 * 10 ^ 2.
+lra.
+Qed.
diff --git a/test-suite/success/RealSyntax.v b/test-suite/success/RealSyntax.v
deleted file mode 100644
index 2765200991..0000000000
--- a/test-suite/success/RealSyntax.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Import Reals.
-Open Scope R_scope.
-Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).
-Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)).
-Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)).
-Check (eq_refl : 1.02e+02 = IZR 102).
-Check (eq_refl : 10.2e-1 = 1.02).
-Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)).
-Check (eq_refl : -0.5 = IZR (-5) / IZR (Z.pow_pos 10 1)).
-
-Goal 254e3 = 2540 * 10 ^ 2.
-ring.
-Qed.
-
-Require Import Psatz.
-
-Goal 254e3 = 2540 * 10 ^ 2.
-lra.
-Qed.
diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
index 855f26698c..4b928007cf 100644
--- a/test-suite/success/Scheme.v
+++ b/test-suite/success/Scheme.v
@@ -25,3 +25,8 @@ Check myeq_rew_fwd_r_dep.
 Set Rewriting Schemes.
 Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true.
 Unset Rewriting Schemes.
+
+(* check that the scheme doesn't minimize itself into something non general *)
+Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
+Lemma bla@{u v|u < v} : foo@{u v} -> False.
+Proof. induction 1. Qed.