aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_13841.v11
-rw-r--r--test-suite/bugs/closed/bug_13896.v24
-rw-r--r--test-suite/bugs/closed/bug_13903.v5
-rw-r--r--test-suite/bugs/closed/bug_13960.v10
-rw-r--r--test-suite/bugs/closed/bug_7631.v6
-rw-r--r--test-suite/ltac2/ind.v25
-rw-r--r--test-suite/output/Notations3.out10
-rw-r--r--test-suite/output/primitive_tokens.out61
-rw-r--r--test-suite/output/primitive_tokens.v23
9 files changed, 169 insertions, 6 deletions
diff --git a/test-suite/bugs/closed/bug_13841.v b/test-suite/bugs/closed/bug_13841.v
new file mode 100644
index 0000000000..60fca8b49c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13841.v
@@ -0,0 +1,11 @@
+Goal True.
+evar (p : bool).
+unify ?p true.
+let v := eval vm_compute in (orb p false) in
+match v with true => idtac end.
+assert (orb p false = true).
+vm_compute.
+match goal with |- true = _ => idtac end.
+easy.
+easy.
+Qed.
diff --git a/test-suite/bugs/closed/bug_13896.v b/test-suite/bugs/closed/bug_13896.v
new file mode 100644
index 0000000000..10f24d8564
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13896.v
@@ -0,0 +1,24 @@
+Inductive type : Set :=
+ Tptr : type -> type
+ | Tref : type -> type
+ | Trv_ref : type -> type
+ | Tint : type -> type -> type
+ | Tvoid : type
+ | Tarray : type -> type -> type
+ | Tnamed : type -> type
+ | Tfunction : type -> type -> type -> type
+ | Tbool : type
+ | Tmember_pointer : type -> type -> type
+ | Tfloat : type -> type
+ | Tqualified : type -> type -> type
+ | Tnullptr : type
+ | Tarch : type -> type -> type
+.
+Definition type_eq_dec : forall (ty1 ty2 : type), { ty1 = ty2 } + { ty1 <> ty2 }.
+Proof. fix IHty1 1. decide equality. Defined.
+
+Goal (if type_eq_dec (Tptr Tvoid) (Tptr Tvoid) then True else False).
+Proof.
+timeout 1 cbn.
+constructor.
+Qed.
diff --git a/test-suite/bugs/closed/bug_13903.v b/test-suite/bugs/closed/bug_13903.v
new file mode 100644
index 0000000000..7c1820b85c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13903.v
@@ -0,0 +1,5 @@
+Section test.
+Variables (T : Type) (x : T).
+#[using="x"] Definition test : unit := tt.
+End test.
+Check test : forall T, T -> unit.
diff --git a/test-suite/bugs/closed/bug_13960.v b/test-suite/bugs/closed/bug_13960.v
new file mode 100644
index 0000000000..947db9586f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13960.v
@@ -0,0 +1,10 @@
+Require Ltac2.Ltac2.
+
+Set Default Goal Selector "!".
+
+Ltac2 t () := let _ := Message.print (Message.of_string "hi") in 42.
+
+Goal False.
+Proof.
+Ltac2 Eval t ().
+Abort.
diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v
index 93aeb83e28..14ab4de9b7 100644
--- a/test-suite/bugs/closed/bug_7631.v
+++ b/test-suite/bugs/closed/bug_7631.v
@@ -21,3 +21,9 @@ Definition bar (x := foo) := Eval native_compute in x.
Definition barvm (x := foo) := Eval vm_compute in x.
End RelContext.
+
+Definition bar (t:=_) (x := true : t) := Eval native_compute in x.
+Definition barvm (t:=_) (x := true : t) := Eval vm_compute in x.
+
+Definition baz (z:nat) (t:=_ z) (x := true : t) := Eval native_compute in x.
+Definition bazvm (z:nat) (t:=_ z) (x := true : t) := Eval vm_compute in x.
diff --git a/test-suite/ltac2/ind.v b/test-suite/ltac2/ind.v
new file mode 100644
index 0000000000..6f7352d224
--- /dev/null
+++ b/test-suite/ltac2/ind.v
@@ -0,0 +1,25 @@
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Option.
+
+Ltac2 Eval
+ let nat := Option.get (Env.get [@Coq; @Init; @Datatypes; @nat]) in
+ let nat := match nat with
+ | Std.IndRef nat => nat
+ | _ => Control.throw Not_found
+ end in
+ let data := Ind.data nat in
+ (* Check that there is only one inductive in the block *)
+ let ntypes := Ind.nblocks data in
+ let () := if Int.equal ntypes 1 then () else Control.throw Not_found in
+ let nat' := Ind.repr (Ind.get_block data 0) in
+ (* Check it corresponds *)
+ let () := if Ind.equal nat nat' then () else Control.throw Not_found in
+ let () := if Int.equal (Ind.index nat) 0 then () else Control.throw Not_found in
+ (* Check the number of constructors *)
+ let nconstr := Ind.nconstructors data in
+ let () := if Int.equal nconstr 2 then () else Control.throw Not_found in
+ (* Create a fresh instance *)
+ let s := Ind.get_constructor data 1 in
+ let s := Env.instantiate (Std.ConstructRef s) in
+ constr:($s 0)
+.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 60213cab0c..cc9e745f6b 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -6,7 +6,7 @@
: nat * nat * (nat * nat)
(0, 2, (2, 2))
: nat * nat * (nat * nat)
-pair (pair O (S (S O))) (pair (S (S O)) O)
+pair (pair 0 2) (pair 2 0)
: prod (prod nat nat) (prod nat nat)
<< 0, 2, 4 >>
: nat * nat * nat * (nat * (nat * nat))
@@ -16,8 +16,7 @@ pair (pair O (S (S O))) (pair (S (S O)) O)
: nat * nat * nat * (nat * (nat * nat))
(0, 2, 4, (0, (2, 4)))
: nat * nat * nat * (nat * (nat * nat))
-pair (pair (pair O (S (S O))) (S (S (S (S O)))))
- (pair (S (S (S (S O)))) (pair (S (S O)) O))
+pair (pair (pair 0 2) 4) (pair 4 (pair 2 0))
: prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
ETA x y : nat, Nat.add
: nat -> nat -> nat
@@ -174,9 +173,8 @@ forall_non_null x y z t : nat , x = y /\ z = t
: nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) *
(nat * nat * nat)
pair
- (pair
- (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O)))
- (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O)))
+ (pair (pair (pair 2 (pair 1 0)) (pair (pair 0 2) 1)) (pair 1 (pair 2 0)))
+ (pair (pair 0 1) 2)
: prod
(prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat))
(prod nat (prod nat nat))) (prod (prod nat nat) nat)
diff --git a/test-suite/output/primitive_tokens.out b/test-suite/output/primitive_tokens.out
new file mode 100644
index 0000000000..afe9b25442
--- /dev/null
+++ b/test-suite/output/primitive_tokens.out
@@ -0,0 +1,61 @@
+"foo"
+ : string
+1234
+ : nat
+Nat.add 1 2
+ : nat
+match "a" with
+| "a" => true
+| _ => false
+end
+ : bool
+match 1 with
+| 1 => true
+| _ => false
+end
+ : bool
+{| field := 7 |}
+ : test
+String (Ascii.Ascii false true true false false true true false)
+ (String (Ascii.Ascii true true true true false true true false)
+ (String (Ascii.Ascii true true true true false true true false)
+ EmptyString))
+ : string
+S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S
+ (S (S (S (S (S (S ...)))))))))))))))))))))))
+ : nat
+Nat.add (S O) (S (S O))
+ : nat
+match
+ String (Ascii.Ascii true false false false false true true false)
+ EmptyString
+with
+| String (Ascii.Ascii true false false false false true true false)
+ EmptyString => true
+| _ => false
+end
+ : bool
+match S O with
+| S O => true
+| _ => false
+end
+ : bool
+{| field := S (S (S (S (S (S (S O)))))) |}
+ : test
diff --git a/test-suite/output/primitive_tokens.v b/test-suite/output/primitive_tokens.v
new file mode 100644
index 0000000000..3207e5983f
--- /dev/null
+++ b/test-suite/output/primitive_tokens.v
@@ -0,0 +1,23 @@
+Require Import String.
+
+Record test := { field : nat }.
+
+Open Scope string_scope.
+
+Unset Printing Notations.
+
+Check "foo".
+Check 1234.
+Check 1 + 2.
+Check match "a" with "a" => true | _ => false end.
+Check match 1 with 1 => true | _ => false end.
+Check {| field := 7 |}.
+
+Set Printing Raw Literals.
+
+Check "foo".
+Check 1234.
+Check 1 + 2.
+Check match "a" with "a" => true | _ => false end.
+Check match 1 with 1 => true | _ => false end.
+Check {| field := 7 |}.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 16:33:13 +0000