aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_11421.v1
-rw-r--r--test-suite/bugs/closed/bug_2729.v2
-rw-r--r--test-suite/complexity/injection.v2
-rw-r--r--test-suite/failure/Template.v22
-rw-r--r--test-suite/output/QArithSyntax.out14
-rw-r--r--test-suite/output/QArithSyntax.v (renamed from test-suite/success/QArithSyntax.v)0
-rw-r--r--test-suite/output/RealSyntax.out14
-rw-r--r--test-suite/output/RealSyntax.v22
-rw-r--r--test-suite/prerequisite/ssr_mini_mathcomp.v6
-rw-r--r--test-suite/success/Inductive.v18
-rw-r--r--test-suite/success/Inversion.v2
-rw-r--r--test-suite/success/RealSyntax.v19
-rw-r--r--test-suite/success/RecTutorial.v4
-rw-r--r--test-suite/success/Scheme.v5
14 files changed, 90 insertions, 41 deletions
diff --git a/test-suite/bugs/closed/bug_11421.v b/test-suite/bugs/closed/bug_11421.v
new file mode 100644
index 0000000000..8ddf05c888
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11421.v
@@ -0,0 +1 @@
+Fail Definition plus1_plus1 : Type@{Set+1} := Type@{Set+1}.
diff --git a/test-suite/bugs/closed/bug_2729.v b/test-suite/bugs/closed/bug_2729.v
index ff08bdc6bb..52cc34beb3 100644
--- a/test-suite/bugs/closed/bug_2729.v
+++ b/test-suite/bugs/closed/bug_2729.v
@@ -82,7 +82,7 @@ Inductive SequenceBase (pu : PatchUniverse)
(p : pu_type from mid)
(qs : SequenceBase pu mid to),
SequenceBase pu from to.
-Arguments Nil [pu cxt].
+Arguments Nil {pu cxt}.
Arguments Cons [pu from mid to].
Program Fixpoint insertBase {pu : PatchUniverse}
diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v
index 298a07c1c4..7022987096 100644
--- a/test-suite/complexity/injection.v
+++ b/test-suite/complexity/injection.v
@@ -47,7 +47,7 @@ Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t),
joinmap key j.
Parameter ADMIT: forall p: Prop, p.
-Arguments ADMIT [p].
+Arguments ADMIT {p}.
Module Share.
Parameter jb : joinable bool.
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/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
index d293dc0533..048fb3b027 100644
--- a/test-suite/prerequisite/ssr_mini_mathcomp.v
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -65,7 +65,7 @@ Proof. by []. Qed.
Lemma eqP T : Equality.axiom (@eq_op T).
Proof. by case: T => ? []. Qed.
-Arguments eqP [T x y].
+Arguments eqP {T x y}.
Delimit Scope eq_scope with EQ.
Open Scope eq_scope.
@@ -345,7 +345,7 @@ Proof. by []. Qed.
End SubEqType.
-Arguments val_eqP [T P sT x y].
+Arguments val_eqP {T P sT x y}.
Prenex Implicits val_eqP.
Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T)
@@ -386,7 +386,7 @@ Qed.
Canonical nat_eqMixin := EqMixin eqnP.
Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
-Arguments eqnP [x y].
+Arguments eqnP {x y}.
Prenex Implicits eqnP.
Coercion nat_of_bool (b : bool) := if b then 1 else 0.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index c2130995fc..4b2d4457bf 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -71,7 +71,7 @@ CoInductive LList (A : Set) : Set :=
| LNil : LList A
| LCons : A -> LList A -> LList A.
-Arguments LNil [A].
+Arguments LNil {A}.
Inductive Finite (A : Set) : LList A -> Prop :=
| Finite_LNil : Finite LNil
@@ -204,3 +204,19 @@ End NonRecLetIn.
Fail Inductive foo (T : Type) : let T := Type in T :=
{ r : forall x : T, x = x }.
+
+Module Discharge.
+ (* discharge test *)
+ Section S.
+ Let x := Prop.
+ Inductive foo : x := bla : foo.
+ End S.
+ Check bla:foo.
+
+ Section S.
+ Variables (A:Type).
+ (* ensure params are scanned for needed section variables even with template arity *)
+ #[universes(template)] Inductive bar (d:A) := .
+ End S.
+ Check @bar nat 0.
+End Discharge.
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 1dbeaf3e1f..8297f54641 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type :=
| in_first : forall e, in_extension r (add_rule r e)
| in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e).
-Arguments NL [I].
+Arguments NL {I}.
Inductive super_extension (I : Set) (e : extension I) :
extension I -> Type :=
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/RecTutorial.v b/test-suite/success/RecTutorial.v
index 4fac798f76..15672eab7c 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -994,7 +994,7 @@ Qed.
Arguments Vector.cons [A] _ [n].
-Arguments Vector.nil [A].
+Arguments Vector.nil {A}.
Arguments Vector.hd [A n].
Arguments Vector.tl [A n].
@@ -1161,7 +1161,7 @@ infiniteproof map_iterate'.
Qed.
-Arguments LNil [A].
+Arguments LNil {A}.
Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
LNil <> (LCons a l).
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:12:46 +0000