aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_11321.v10
-rw-r--r--test-suite/output/Cases.out12
-rw-r--r--test-suite/output/Cases.v20
-rw-r--r--test-suite/output/PrintCanonicalProjections.out18
-rw-r--r--test-suite/output/PrintCanonicalProjections.v46
-rw-r--r--test-suite/output/unification.out11
-rw-r--r--test-suite/output/unification.v12
-rw-r--r--test-suite/success/Omega.v2
-rw-r--r--test-suite/success/OmegaPre.v40
-rw-r--r--test-suite/success/custom_entry.v13
10 files changed, 163 insertions, 21 deletions
diff --git a/test-suite/bugs/closed/bug_11321.v b/test-suite/bugs/closed/bug_11321.v
new file mode 100644
index 0000000000..ce95280fb1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11321.v
@@ -0,0 +1,10 @@
+Require Import Cyclic63.
+
+Goal False.
+Proof.
+assert (4294967296 *c 2147483648 = WW 2 0)%int63 as H.
+ vm_cast_no_check (@eq_refl (zn2z int) (WW 2 0)%int63).
+generalize (f_equal (zn2z_to_Z wB to_Z) H).
+now rewrite mulc_WW_spec.
+Fail Qed.
+Abort.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index e84ac85aa8..6976610b22 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -166,3 +166,15 @@ fun x : K => match x with
: K -> nat
The command has indeed failed with message:
Pattern "S _, _" is redundant in this clause.
+stray =
+fun N : Tree =>
+match N with
+| App (App Node (Node as strayvariable)) _ |
+ App (App Node (App Node _ as strayvariable)) _ |
+ App (App Node (App (App Node Node) (App _ _) as strayvariable)) _ |
+ App (App Node (App (App Node (App _ _)) _ as strayvariable)) _ |
+ App (App Node (App (App (App _ _) _) _ as strayvariable)) _ =>
+ strayvariable
+| _ => Node
+end
+ : Tree -> Tree
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index a040b69b44..262ec2b677 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -222,3 +222,23 @@ Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end.
(* Test redundant clause within a disjunctive pattern *)
Fail Check fun n m => match n, m with 0, 0 | _, S _ | S 0, _ | S (S _ | _), _ => false end.
+
+Module Bug11231.
+
+(* Missing dependency in computing if a clause is a default clause *)
+
+Inductive Tree: Set :=
+| Node : Tree
+| App : Tree -> Tree -> Tree
+.
+
+Definition stray N :=
+match N with
+| App (App Node (App (App Node Node) Node)) _ => Node
+| App (App Node strayvariable) _ => strayvariable
+| _ => Node
+end.
+
+Print stray.
+
+End Bug11231.
diff --git a/test-suite/output/PrintCanonicalProjections.out b/test-suite/output/PrintCanonicalProjections.out
new file mode 100644
index 0000000000..a4e2251440
--- /dev/null
+++ b/test-suite/output/PrintCanonicalProjections.out
@@ -0,0 +1,18 @@
+bool <- sort_eq ( bool_eqType )
+bool <- sort_TYPE ( bool_TYPE )
+nat <- sort_eq ( nat_eqType )
+nat <- sort_TYPE ( nat_TYPE )
+prod <- sort_eq ( prod_eqType )
+prod <- sort_TYPE ( prod_TYPE )
+sum <- sort_eq ( sum_eqType )
+sum <- sort_TYPE ( sum_TYPE )
+sum <- sort_TYPE ( sum_TYPE )
+prod <- sort_TYPE ( prod_TYPE )
+nat <- sort_TYPE ( nat_TYPE )
+bool <- sort_TYPE ( bool_TYPE )
+sum <- sort_eq ( sum_eqType )
+prod <- sort_eq ( prod_eqType )
+nat <- sort_eq ( nat_eqType )
+bool <- sort_eq ( bool_eqType )
+bool <- sort_TYPE ( bool_TYPE )
+bool <- sort_eq ( bool_eqType )
diff --git a/test-suite/output/PrintCanonicalProjections.v b/test-suite/output/PrintCanonicalProjections.v
new file mode 100644
index 0000000000..808cdffe39
--- /dev/null
+++ b/test-suite/output/PrintCanonicalProjections.v
@@ -0,0 +1,46 @@
+Record TYPE := Pack_TYPE { sort_TYPE :> Type }.
+Record eqType := Pack_eq { sort_eq :> Type; _ : sort_eq -> sort_eq -> bool }.
+
+Definition eq_op (T : eqType) : T -> T -> bool :=
+ match T with Pack_eq _ op => op end.
+
+Definition bool_eqb b1 b2 :=
+ match b1, b2 with
+ | false, false => true
+ | true, true => true
+ | _, _ => false
+ end.
+
+Canonical bool_TYPE := Pack_TYPE bool.
+Canonical bool_eqType := Pack_eq bool bool_eqb.
+
+Canonical nat_TYPE := Pack_TYPE nat.
+Canonical nat_eqType := Pack_eq nat Nat.eqb.
+
+Definition prod_eqb (T U : eqType) (x y : T * U) :=
+ match x, y with
+ | (x1, x2), (y1, y2) =>
+ andb (eq_op _ x1 y1) (eq_op _ x2 y2)
+ end.
+
+Canonical prod_TYPE (T U : TYPE) := Pack_TYPE (T * U).
+Canonical prod_eqType (T U : eqType) := Pack_eq (T * U) (prod_eqb T U).
+
+Definition sum_eqb (T U : eqType) (x y : T + U) :=
+ match x, y with
+ | inl x, inl y => eq_op _ x y
+ | inr x, inr y => eq_op _ x y
+ | _, _ => false
+ end.
+
+Canonical sum_TYPE (T U : TYPE) := Pack_TYPE (T + U).
+Canonical sum_eqType (T U : eqType) := Pack_eq (T + U) (sum_eqb T U).
+
+Print Canonical Projections bool.
+Print Canonical Projections nat.
+Print Canonical Projections prod.
+Print Canonical Projections sum.
+Print Canonical Projections sort_TYPE.
+Print Canonical Projections sort_eq.
+Print Canonical Projections sort_TYPE bool.
+Print Canonical Projections bool_eqType.
diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out
new file mode 100644
index 0000000000..dfd755da61
--- /dev/null
+++ b/test-suite/output/unification.out
@@ -0,0 +1,11 @@
+The command has indeed failed with message:
+In environment
+x : T
+T : Type
+a : T
+Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate
+"?X" because "T" is not in its scope: available arguments are
+"x" "C a").
+The command has indeed failed with message:
+The term "id" has type "ID" while it is expected to have type
+"Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope).
diff --git a/test-suite/output/unification.v b/test-suite/output/unification.v
new file mode 100644
index 0000000000..ff99f2e23c
--- /dev/null
+++ b/test-suite/output/unification.v
@@ -0,0 +1,12 @@
+(* Unification error tests *)
+
+Module A.
+
+(* Check regression of an UNBOUND_REL bug *)
+Inductive T := C : forall {A}, A -> T.
+Fail Check fun x => match x return ?[X] with C a => a end.
+
+(* Bug #3634 *)
+Fail Check (id:Type -> _).
+
+End A.
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index 470e4f0580..5e0f90d59b 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -90,5 +90,5 @@ Qed.
(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
Lemma lem10 : forall n m:nat, le n (plus n (mult n m)).
Proof.
-intros; omega with *.
+intros; zify; omega.
Qed.
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v
index 17531064cc..0223255067 100644
--- a/test-suite/success/OmegaPre.v
+++ b/test-suite/success/OmegaPre.v
@@ -16,112 +16,112 @@ Open Scope Z_scope.
Goal forall a:Z, Z.max a a = a.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall a b:Z, Z.max a b = Z.max b a.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
intros.
zify.
-intuition; subst; omega. (* pure multiplication: omega alone can't do it *)
+intuition; subst; zify; omega. (* pure multiplication: zify; omega alone can't do it *)
Qed.
Goal forall a:Z, Z.abs a = a -> a >= 0.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
intros.
-omega with *.
+zify; omega.
Qed.
(* zify_nat *)
Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
intros.
-omega with *.
+zify; omega.
Qed.
(* 2000 instead of 200: works, but quite slow *)
Goal forall m: nat, (m*m>=0)%nat.
intros.
-omega with *.
+zify; omega.
Qed.
(* zify_positive *)
Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall m: positive, (m*m>=1)%positive.
intros.
-omega with *.
+zify; omega.
Qed.
(* zify_N *)
Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall m:N, (m<1)%N -> (m=0)%N.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
intros.
-omega with *.
+zify; omega.
Qed.
Goal forall m:N, (m*m>=0)%N.
intros.
-omega with *.
+zify; omega.
Qed.
(* mix of datatypes *)
Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
intros.
-omega with *.
+zify; omega.
Qed.
diff --git a/test-suite/success/custom_entry.v b/test-suite/success/custom_entry.v
new file mode 100644
index 0000000000..e88ae65e18
--- /dev/null
+++ b/test-suite/success/custom_entry.v
@@ -0,0 +1,13 @@
+Declare Custom Entry foo.
+
+Print Custom Grammar foo.
+
+Notation "[ e ]" := e (e custom foo at level 0).
+
+Print Custom Grammar foo.
+
+Notation "1" := O (in custom foo at level 0).
+
+Print Custom Grammar foo.
+
+Fail Declare Custom Entry foo.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 04:16:34 +0000