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/evar.v17
-rw-r--r--test-suite/ltac2/ind.v25
-rw-r--r--test-suite/ltac2/rebind.v4
-rw-r--r--test-suite/ltac2/syntax_cast.v14
-rw-r--r--test-suite/output/Notations3.out10
-rw-r--r--test-suite/output/ltac2_deprecated.out12
-rw-r--r--test-suite/output/ltac2_deprecated.v15
-rw-r--r--test-suite/output/primitive_tokens.out61
-rw-r--r--test-suite/output/primitive_tokens.v23
-rw-r--r--test-suite/output/relaxed_ambiguous_paths.out20
15 files changed, 238 insertions, 19 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/evar.v b/test-suite/ltac2/evar.v
new file mode 100644
index 0000000000..2c82673edd
--- /dev/null
+++ b/test-suite/ltac2/evar.v
@@ -0,0 +1,17 @@
+Require Import Ltac2.Ltac2.
+
+Goal exists (a: nat), a = 1.
+Proof.
+ match! goal with
+ | [ |- ?g ] => Control.assert_false (Constr.has_evar g)
+ end.
+ eexists.
+ match! goal with
+ | [ |- ?g ] => Control.assert_true (Constr.has_evar g)
+ end.
+ match! goal with
+ | [ |- ?x = ?y ] =>
+ Control.assert_true (Constr.is_evar x);
+ Control.assert_false (Constr.is_evar y)
+ end.
+Abort.
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/ltac2/rebind.v b/test-suite/ltac2/rebind.v
index 7b3a460c8c..9108871e28 100644
--- a/test-suite/ltac2/rebind.v
+++ b/test-suite/ltac2/rebind.v
@@ -26,12 +26,10 @@ Ltac2 rec nat_eq n m :=
| S n => match m with | O => false | S m => nat_eq n m end
end.
-Ltac2 Type exn ::= [ Assertion_failed ].
-
Ltac2 assert_eq n m :=
match nat_eq n m with
| true => ()
- | false => Control.throw Assertion_failed end.
+ | false => Control.throw Assertion_failure end.
Ltac2 mutable x := O.
Ltac2 y := x.
diff --git a/test-suite/ltac2/syntax_cast.v b/test-suite/ltac2/syntax_cast.v
new file mode 100644
index 0000000000..f62d49173d
--- /dev/null
+++ b/test-suite/ltac2/syntax_cast.v
@@ -0,0 +1,14 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 foo0 x y : unit := ().
+Ltac2 foo1 : unit := ().
+Fail Ltac2 foo2 : unit -> unit := ().
+Ltac2 foo3 : unit -> unit := fun (_ : unit) => ().
+
+Ltac2 bar0 := fun x y : unit => ().
+Fail Ltac2 bar1 := fun x : unit => 0.
+Ltac2 bar2 := fun x : unit list => [].
+
+Ltac2 qux0 := let x : unit := () in ().
+Ltac2 qux1 () := let x y z : unit := () in x 0 "".
+Fail Ltac2 qux2 := let x : unit -> unit := () in ().
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/ltac2_deprecated.out b/test-suite/output/ltac2_deprecated.out
new file mode 100644
index 0000000000..d17b719bcd
--- /dev/null
+++ b/test-suite/output/ltac2_deprecated.out
@@ -0,0 +1,12 @@
+File "stdin", line 13, characters 11-14:
+Warning: Ltac2 definition foo is deprecated. test_definition
+[deprecated-ltac2-definition,deprecated]
+- : unit = ()
+File "stdin", line 14, characters 11-14:
+Warning: Ltac2 alias bar is deprecated. test_notation
+[deprecated-ltac2-alias,deprecated]
+- : unit = ()
+File "stdin", line 15, characters 11-14:
+Warning: Ltac2 definition qux is deprecated. test_external
+[deprecated-ltac2-definition,deprecated]
+- : 'a array -> int = <fun>
diff --git a/test-suite/output/ltac2_deprecated.v b/test-suite/output/ltac2_deprecated.v
new file mode 100644
index 0000000000..9598a5979c
--- /dev/null
+++ b/test-suite/output/ltac2_deprecated.v
@@ -0,0 +1,15 @@
+Require Import Ltac2.Ltac2.
+
+#[deprecated(note="test_definition")]
+Ltac2 foo := ().
+
+#[deprecated(note="test_notation")]
+Ltac2 Notation bar := ().
+
+#[deprecated(note="test_external")]
+Ltac2 @ external qux : 'a array -> int := "ltac2" "array_length".
+(* Randomly picked external function *)
+
+Ltac2 Eval foo.
+Ltac2 Eval bar.
+Ltac2 Eval qux.
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 |}.
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
index ac5a09bad7..48368c7ede 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -3,32 +3,32 @@ Warning:
New coercion path [ac; cd] : A >-> D is ambiguous with existing
[ab; bd] : A >-> D. [ambiguous-paths,typechecker]
[ab] : A >-> B
-[ab; bd] : A >-> D
[ac] : A >-> C
+[ab; bd] : A >-> D
[bd] : B >-> D
[cd] : C >-> D
File "stdin", line 26, characters 0-28:
Warning:
New coercion path [ab; bc] : A >-> C is ambiguous with existing
[ac] : A >-> C. [ambiguous-paths,typechecker]
+[ab] : A >-> B
[ac] : A >-> C
[ac; cd] : A >-> D
-[ab] : A >-> B
-[cd] : C >-> D
[bc] : B >-> C
[bc; cd] : B >-> D
+[cd] : C >-> D
[B_A] : B >-> A
[C_A] : C >-> A
-[D_B] : D >-> B
[D_A] : D >-> A
+[D_B] : D >-> B
[D_C] : D >-> C
[A'_A] : A' >-> A
-[B_A'] : B >-> A'
[B_A'; A'_A] : B >-> A
-[C_A'] : C >-> A'
+[B_A'] : B >-> A'
[C_A'; A'_A] : C >-> A
-[D_B; B_A'] : D >-> A'
+[C_A'] : C >-> A'
[D_A] : D >-> A
+[D_B; B_A'] : D >-> A'
[D_B] : D >-> B
[D_C] : D >-> C
File "stdin", line 121, characters 0-86:
@@ -36,12 +36,12 @@ Warning:
New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
[D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker]
[A'_A] : A' >-> A
-[B_A'] : B >-> A'
[B_A'; A'_A] : B >-> A
-[C_A'] : C >-> A'
+[B_A'] : B >-> A'
[C_A'; A'_A] : C >-> A
-[D_B; B_A'] : D >-> A'
+[C_A'] : C >-> A'
[D_A] : D >-> A
+[D_B; B_A'] : D >-> A'
[D_B] : D >-> B
[D_C] : D >-> C
File "stdin", line 130, characters 0-47:
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 20:11:03 +0000