aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs')
-rw-r--r--test-suite/bugs/closed/HoTT_coq_107.v1
-rw-r--r--test-suite/bugs/closed/bug_12045.v19
-rw-r--r--test-suite/bugs/closed/bug_12196.v46
-rw-r--r--test-suite/bugs/closed/bug_12257.v3
-rw-r--r--test-suite/bugs/closed/bug_3881.v1
-rw-r--r--test-suite/bugs/closed/bug_4527.v2
-rw-r--r--test-suite/bugs/closed/bug_4533.v2
-rw-r--r--test-suite/bugs/closed/bug_4544.v2
-rw-r--r--test-suite/bugs/closed/bug_5359.v4
-rw-r--r--test-suite/bugs/closed/bug_5445.v11
-rw-r--r--test-suite/bugs/closed/bug_6378.v9
-rw-r--r--test-suite/bugs/closed/bug_6661.v1
-rw-r--r--test-suite/bugs/closed/bug_7812.v30
13 files changed, 126 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v
index fa4072a8f6..91f5c423a5 100644
--- a/test-suite/bugs/closed/HoTT_coq_107.v
+++ b/test-suite/bugs/closed/HoTT_coq_107.v
@@ -2,6 +2,7 @@
(* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *)
(** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *)
Require Import Coq.Init.Logic.
+Require Import Coq.Init.Ltac.
Global Set Universe Polymorphism.
Global Set Asymmetric Patterns.
Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/bug_12045.v b/test-suite/bugs/closed/bug_12045.v
new file mode 100644
index 0000000000..4e416778a9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12045.v
@@ -0,0 +1,19 @@
+(* Check enough reduction happens in the conclusion of an induction scheme *)
+
+Lemma foo :
+ forall (P : nat -> Prop),
+ (forall n, P (S n)) ->
+ forall n,
+ (fun e =>
+ IsSucc e ->
+ P e) n.
+Proof.
+Admitted.
+
+Theorem bar : forall n,
+ IsSucc n ->
+ True.
+Proof.
+ intros.
+ Fail induction n using foo. (* was an anomaly *)
+Admitted.
diff --git a/test-suite/bugs/closed/bug_12196.v b/test-suite/bugs/closed/bug_12196.v
new file mode 100644
index 0000000000..c0851b3204
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12196.v
@@ -0,0 +1,46 @@
+(** TODO: Figure out how to test "sanity" for the ltac profiler output *)
+Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end.
+Fixpoint walk (n : nat) := match n with 0 => tt | S n => walk n end.
+Ltac slow := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)).
+Ltac slow2 := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)).
+Ltac multi := idtac + slow + slow2.
+Set Ltac Profiling.
+Goal True.
+ Time try (multi; fail).
+ (* Warning: Ltac Profiler cannot yet handle backtracking into multi-success
+ tactics; profiling results may be wildly inaccurate.
+ [profile-backtracking,ltac] *)
+ Show Ltac Profile.
+ (* Used to be:
+total time: 0.000s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi --------------------------------- 47.1% 47.1% 1 0.000s
+─slow ---------------------------------- 35.3% 35.3% 1 0.000s
+─slow2 --------------------------------- 17.6% 17.6% 1 0.000s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi --------------------------------- 47.1% 47.1% 1 0.000s
+─slow ---------------------------------- 35.3% 35.3% 1 0.000s
+─slow2 --------------------------------- 17.6% 17.6% 1 0.000s
+
+ *)
+ (* Now:
+total time: 2.074s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi --------------------------------- 0.0% 100.0% 6 1.119s
+─slow ---------------------------------- 54.0% 54.0% 3 1.119s
+─slow2 --------------------------------- 46.0% 46.0% 3 0.955s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi --------------------------------- 0.0% 100.0% 6 1.119s
+ ├─slow -------------------------------- 54.0% 54.0% 3 1.119s
+ └─slow2 ------------------------------- 46.0% 46.0% 3 0.955s
+
+*)
+Abort.
diff --git a/test-suite/bugs/closed/bug_12257.v b/test-suite/bugs/closed/bug_12257.v
new file mode 100644
index 0000000000..4962048a42
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12257.v
@@ -0,0 +1,3 @@
+(* Test that ExtrHaskellString transitively requires ExtrHaskellBasic *)
+Require Coq.extraction.ExtrHaskellString.
+Import Coq.extraction.ExtrHaskellBasic.
diff --git a/test-suite/bugs/closed/bug_3881.v b/test-suite/bugs/closed/bug_3881.v
index d7e097e326..50e9de60e5 100644
--- a/test-suite/bugs/closed/bug_3881.v
+++ b/test-suite/bugs/closed/bug_3881.v
@@ -4,6 +4,7 @@
coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *)
Generalizable All Variables.
Require Import Coq.Init.Notations.
+Require Import Coq.Init.Ltac.
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Axiom admit : forall {T}, T.
diff --git a/test-suite/bugs/closed/bug_4527.v b/test-suite/bugs/closed/bug_4527.v
index dfb07520f1..cf802eb89b 100644
--- a/test-suite/bugs/closed/bug_4527.v
+++ b/test-suite/bugs/closed/bug_4527.v
@@ -5,7 +5,7 @@ then from 269 lines to 255 lines *)
(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml
4.01.0
coqtop version 8.5 (January 2016) *)
-Declare ML Module "ltac_plugin".
+Require Import Coq.Init.Ltac.
Inductive False := .
Axiom proof_admitted : False.
Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/bug_4533.v b/test-suite/bugs/closed/bug_4533.v
index d2f9fb9099..2d628f414d 100644
--- a/test-suite/bugs/closed/bug_4533.v
+++ b/test-suite/bugs/closed/bug_4533.v
@@ -5,7 +5,7 @@ then from 285 lines to 271 lines *)
(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml
4.01.0
coqtop version 8.5 (January 2016) *)
-Declare ML Module "ltac_plugin".
+Require Import Coq.Init.Ltac.
Inductive False := .
Axiom proof_admitted : False.
Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/bug_4544.v b/test-suite/bugs/closed/bug_4544.v
index e9e9c552f6..213c91bfa0 100644
--- a/test-suite/bugs/closed/bug_4544.v
+++ b/test-suite/bugs/closed/bug_4544.v
@@ -2,7 +2,7 @@
(* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *)
(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0
coqtop version 8.5 (January 2016) *)
-Declare ML Module "ltac_plugin".
+Require Import Coq.Init.Ltac.
Inductive False := .
Axiom proof_admitted : False.
Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/bug_5359.v b/test-suite/bugs/closed/bug_5359.v
index 1f202e4396..36f2ec5891 100644
--- a/test-suite/bugs/closed/bug_5359.v
+++ b/test-suite/bugs/closed/bug_5359.v
@@ -90,7 +90,7 @@ Goal False.
(Ring_polynom.PEX Z 2)))
(Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
(Ring_polynom.PEX Z 3)))) :: nil)%list ) in
- Nsatz.nsatz_compute
+ NsatzTactic.nsatz_compute
(@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))).
let sugar := constr:( 0%Z ) in
@@ -214,6 +214,6 @@ Goal False.
(Ring_polynom.PEX Z 2)))
(Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
(Ring_polynom.PEX Z 3)))) :: nil)%list ) in
- Nsatz.nsatz_compute
+ NsatzTactic.nsatz_compute
(@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))).
Abort.
diff --git a/test-suite/bugs/closed/bug_5445.v b/test-suite/bugs/closed/bug_5445.v
new file mode 100644
index 0000000000..deaf174661
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5445.v
@@ -0,0 +1,11 @@
+Require Import Coq.nsatz.NsatzTactic.
+(** Ensure that loading the nsatz tactic doesn't load the reals *)
+Fail Module M := Coq.Reals.Rdefinitions.
+(** Ensure that loading the nsatz tactic doesn't load classic *)
+Fail Check Coq.Logic.Classical_Prop.classic.
+(** Ensure that this test-case hasn't messed up about the location of the reals / how to check for them *)
+Require Coq.Reals.Rdefinitions.
+Module M := Coq.Reals.Rdefinitions.
+(** Ensure that this test-case hasn't messed up about the location of classic / how to check for it *)
+Require Coq.Logic.Classical_Prop.
+Check Coq.Logic.Classical_Prop.classic.
diff --git a/test-suite/bugs/closed/bug_6378.v b/test-suite/bugs/closed/bug_6378.v
index 68ae7961dd..453924d587 100644
--- a/test-suite/bugs/closed/bug_6378.v
+++ b/test-suite/bugs/closed/bug_6378.v
@@ -7,11 +7,20 @@ Ltac profile_constr tac :=
Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl).
+Ltac manipulate_ltac_prof :=
+ start ltac profiling;
+ reset ltac profile;
+ try ((idtac + reset ltac profile + idtac); fail);
+ try ((idtac + start ltac profiling + idtac); fail);
+ try ((idtac + stop ltac profiling + idtac); fail).
+
Goal True.
start ltac profiling.
reset ltac profile.
+ manipulate_ltac_prof.
reset ltac profile.
stop ltac profiling.
+ Set Warnings Append "+profile-invalid-stack-no-self".
time profile_constr slow.
show ltac profile cutoff 0.
show ltac profile "slow".
diff --git a/test-suite/bugs/closed/bug_6661.v b/test-suite/bugs/closed/bug_6661.v
index 28a9ffc7bd..0f4ae2b4c5 100644
--- a/test-suite/bugs/closed/bug_6661.v
+++ b/test-suite/bugs/closed/bug_6661.v
@@ -7,6 +7,7 @@
Require Export Coq.Init.Notations.
+Require Export Coq.Init.Ltac.
Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
diff --git a/test-suite/bugs/closed/bug_7812.v b/test-suite/bugs/closed/bug_7812.v
new file mode 100644
index 0000000000..a714eea81d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_7812.v
@@ -0,0 +1,30 @@
+Module Foo.
+ Definition binary A := A -> A -> Prop.
+
+ Definition inter A (R1 R2 : binary A): binary A :=
+ fun (x y:A) => R1 x y /\ R2 x y.
+End Foo.
+
+Module Simple_sparse_proof.
+ Parameter node : Type.
+ Parameter graph : Type.
+ Parameter has_edge : graph -> node -> node -> Prop.
+ Implicit Types x y z : node.
+ Implicit Types G : graph.
+
+ Parameter mem : forall A, A -> list A -> Prop.
+ Hypothesis mem_nil : forall x, mem node x nil = False.
+
+ Definition notin (l: list node): node -> node -> Prop :=
+ fun x y => ~ mem node x l /\ ~ mem node y l.
+
+ Definition edge_notin G l : node -> node -> Prop :=
+ Foo.inter node (has_edge G) (notin l).
+
+ Hint Unfold Foo.inter notin edge_notin : rel_crush.
+
+ Lemma edge_notin_nil G : forall x y, edge_notin G nil x y <-> has_edge G x y.
+ Proof.
+ intros. autounfold with rel_crush. rewrite !mem_nil. tauto.
+ Qed.
+End Simple_sparse_proof.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 00:33:03 +0000