aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile4
-rw-r--r--test-suite/bugs/closed/2733.v15
-rw-r--r--test-suite/bugs/closed/8119.v46
-rw-r--r--test-suite/bugs/closed/8126.v13
-rw-r--r--test-suite/output/BadOptionValueType.out8
-rw-r--r--test-suite/output/BadOptionValueType.v4
-rw-r--r--test-suite/output/Cases.out2
-rw-r--r--test-suite/output/Cases.v3
-rw-r--r--test-suite/output/Notations3.out6
-rw-r--r--test-suite/output/Notations3.v11
10 files changed, 108 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 33b4023272..b8aac8b6f8 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -192,10 +192,6 @@ PRINT_LOGS?=
TRAVIS?= # special because we want to print travis_fold directives
ifdef APPVEYOR
PRINT_LOGS:=APPVEYOR
-else
-ifdef CIRCLECI
-PRINT_LOGS:=CIRCLECI
-endif #CIRCLECI
endif #APPVEYOR
report: summary.log
diff --git a/test-suite/bugs/closed/2733.v b/test-suite/bugs/closed/2733.v
index 832de4f913..24dd30b32e 100644
--- a/test-suite/bugs/closed/2733.v
+++ b/test-suite/bugs/closed/2733.v
@@ -16,6 +16,21 @@ match k,l with
|B,l' => Bcons true (Ncons 0 l')
end.
+(* At some time, the success of trullynul was dependent on the name of
+ the variables! *)
+
+Definition trullynul2 k {a} (l : alt_list k a) :=
+match k,l with
+ |N,l' => Ncons 0 (Bcons true l')
+ |B,l' => Bcons true (Ncons 0 l')
+end.
+
+Definition trullynul3 k {z} (l : alt_list k z) :=
+match k,l with
+ |N,l' => Ncons 0 (Bcons true l')
+ |B,l' => Bcons true (Ncons 0 l')
+end.
+
Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 ->
alt_list t1 t3 :=
match l with
diff --git a/test-suite/bugs/closed/8119.v b/test-suite/bugs/closed/8119.v
new file mode 100644
index 0000000000..c6329a7328
--- /dev/null
+++ b/test-suite/bugs/closed/8119.v
@@ -0,0 +1,46 @@
+Require Import Coq.Strings.String.
+
+Section T.
+ Eval vm_compute in let x := tt in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+ Eval vm_compute in let _ := Set in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+ Eval vm_compute in let _ := Prop in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+End T.
+
+Section U0.
+ Let n : unit := tt.
+ Eval vm_compute in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+ Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+End U0.
+
+Section S0.
+ Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "".
+ Eval vm_compute in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+ Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+End S0.
+
+Class T := { }.
+Section S1.
+ Context {p : T}.
+ Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "".
+ Eval vm_compute in _.
+(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)
+ Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort.
+(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)
+End S1.
+
+Class M := { m : Type }.
+Section S2.
+ Context {p : M}.
+ Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "".
+ Eval vm_compute in _.
+(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *)
+ Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort.
+(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *)
+End S2.
diff --git a/test-suite/bugs/closed/8126.v b/test-suite/bugs/closed/8126.v
new file mode 100644
index 0000000000..f52dfc6b47
--- /dev/null
+++ b/test-suite/bugs/closed/8126.v
@@ -0,0 +1,13 @@
+(* See also output test Notations4.v *)
+
+Inductive foo := tt.
+Bind Scope foo_scope with foo.
+Delimit Scope foo_scope with foo.
+Notation "'HI'" := tt : foo_scope.
+Definition myfoo (x : nat) (y : nat) (z : foo) := y.
+Notation myfoo0 := (@myfoo 0).
+Notation myfoo01 := (@myfoo0 1).
+Check myfoo 0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *)
+Check myfoo0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *)
+Check myfoo01 tt. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *)
+Check myfoo01 HI. (* was failing *)
diff --git a/test-suite/output/BadOptionValueType.out b/test-suite/output/BadOptionValueType.out
new file mode 100644
index 0000000000..34d8518a75
--- /dev/null
+++ b/test-suite/output/BadOptionValueType.out
@@ -0,0 +1,8 @@
+The command has indeed failed with message:
+Bad type of value for this option: expected int, got string.
+The command has indeed failed with message:
+Bad type of value for this option: expected bool, got string.
+The command has indeed failed with message:
+Bad type of value for this option: expected bool, got int.
+The command has indeed failed with message:
+Bad type of value for this option: expected bool, got int.
diff --git a/test-suite/output/BadOptionValueType.v b/test-suite/output/BadOptionValueType.v
new file mode 100644
index 0000000000..b61c3757ba
--- /dev/null
+++ b/test-suite/output/BadOptionValueType.v
@@ -0,0 +1,4 @@
+Fail Set Default Timeout "2".
+Fail Set Debug Eauto "yes".
+Fail Set Debug Eauto 1.
+Fail Set Implicit Arguments 1.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 419dcadb4c..dfab400baa 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -169,3 +169,5 @@ fun x : K => match x with
| _ => 2
end
: K -> nat
+The command has indeed failed with message:
+Pattern "S _, _" is redundant in this clause.
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4740c009a4..e4fa7044e7 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -217,3 +217,6 @@ Check fun x => match x with a3 | a4 => 3 | _ => 2 end.
Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end.
Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end.
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.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 5ab616160a..d32cf67e28 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -246,3 +246,9 @@ Notation
============================
##@%
^^^
+myfoo01 tt
+ : nat
+myfoo01 tt
+ : nat
+myfoo01 tt
+ : nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 876aaa3944..180e8d337e 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -399,3 +399,14 @@ Show.
Abort.
End Issue7731.
+
+Module Issue8126.
+
+Definition myfoo (x : nat) (y : nat) (z : unit) := y.
+Notation myfoo0 := (@myfoo 0).
+Notation myfoo01 := (@myfoo0 1).
+Check myfoo 0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *)
+Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *)
+Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *)
+
+End Issue8126.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 09:05:07 +0000