From c694b91bba898aad1e071d91fa70b7c5574cbf98 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Sep 2016 17:42:53 +0200
Subject: Fix bug 4969, autoapply was not tagging shelved subgoals correctly as
 unresolvable

---
 test-suite/bugs/closed/4969.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/4969.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4969.v b/test-suite/bugs/closed/4969.v
new file mode 100644
index 0000000000..4dee41e221
--- /dev/null
+++ b/test-suite/bugs/closed/4969.v
@@ -0,0 +1,11 @@
+Require Import Classes.Init.
+
+Class C A := c : A.
+Instance nat_C : C nat := 0.
+Instance bool_C : C bool := true.
+Lemma silly {A} `{C A} : 0 = 0 -> c = c -> True.
+Proof. auto. Qed.
+
+Goal True.
+  class_apply @silly; [reflexivity|].
+  reflexivity. Fail Qed.
-- 
cgit v1.2.3


From ed9ab22b8c3b2210f479689f46d3e4b2fd4f52df Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 17 Dec 2016 13:00:55 +0100
Subject: Add test-suite files for hintdb variables in Ltac.

In particular, this closes bug 2417.
---
 test-suite/bugs/closed/2417.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/2417.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v
new file mode 100644
index 0000000000..b2f00ffc65
--- /dev/null
+++ b/test-suite/bugs/closed/2417.v
@@ -0,0 +1,15 @@
+Parameter x y : nat.
+Axiom H : x = y.
+Hint Rewrite H : mybase.
+
+Ltac bar base := autorewrite with base.
+
+Tactic Notation "foo" ident(base) := autorewrite with base.
+
+Goal x = 0.
+  bar mybase.
+  now_show (y = 0).
+  Undo 2.
+  foo mybase.
+  now_show (y = 0).
+Abort.
-- 
cgit v1.2.3


From 0b8d185baab95d92a7779482c7861c7be0a8e979 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 9 Feb 2017 18:26:33 +0100
Subject: Fixing bug #5346 (an unimplemented application of 'pat).

---
 test-suite/bugs/closed/5346.v | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 test-suite/bugs/closed/5346.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5346.v b/test-suite/bugs/closed/5346.v
new file mode 100644
index 0000000000..0118c18704
--- /dev/null
+++ b/test-suite/bugs/closed/5346.v
@@ -0,0 +1,29 @@
+Inductive comp : Type -> Type :=
+| Ret {T} : forall (v:T), comp T
+| Bind {T T'} : forall (p: comp T') (p': T' -> comp T), comp T.
+
+Notation "'do' x .. y <- p1 ; p2" :=
+  (Bind p1 (fun x => .. (fun y => p2) ..))
+    (at level 60, right associativity,
+     x binder, y binder).
+
+Definition Fst1 A B (p: comp (A*B)) : comp A :=
+  do '(a, b) <- p;
+    Ret a.
+
+Definition Fst2 A B (p: comp (A*B)) : comp A :=
+  match tt with
+  | _ => Bind p (fun '(a, b) => Ret a)
+  end.
+
+Definition Fst3 A B (p: comp (A*B)) : comp A :=
+  match tt with
+  | _ => do a <- p;
+          Ret (fst a)
+  end.
+
+Definition Fst A B (p: comp (A * B)) : comp A :=
+  match tt with
+  | _ => do '(a, b) <- p;
+          Ret a
+  end.
-- 
cgit v1.2.3


From ebc0870ca932acf0ceea5fe513e2ca40e74c2a02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Oct 2016 17:34:12 +0200
Subject: Moving the Ltac plugin to a pack-based one.

This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
---
 test-suite/bugs/closed/3612.v | 3 +++
 test-suite/bugs/closed/3649.v | 2 ++
 test-suite/bugs/closed/4121.v | 4 +++-
 test-suite/bugs/closed/4527.v | 1 +
 test-suite/bugs/closed/4533.v | 3 ++-
 test-suite/bugs/closed/4544.v | 3 ++-
 6 files changed, 13 insertions(+), 3 deletions(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index a547685070..4b4f81dbce 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -38,8 +38,11 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
            (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
 p = q.
 
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
 
+Set Default Proof Mode "Classic".
+
 Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
             (xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
        @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index fc4c171e2c..8687eaab00 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -2,7 +2,9 @@
 (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
+Set Default Proof Mode "Classic".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
 Delimit Scope type_scope with type.
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index d34a2b8b1b..816bc845fd 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -4,6 +4,8 @@ Unset Strict Universe Declaration.
 (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *)
 
+Declare ML Module "ltac_plugin".
+
 Set Universe Polymorphism.
 Class Contr_internal (A : Type) := BuildContr { center : A }.
 Arguments center A {_}.
@@ -13,4 +15,4 @@ Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A
 Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}.
 Check @contr_paths_contr0@{i}.
 Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *)
-(** It should have length 1, just like contr_paths_contr0 *)
\ No newline at end of file
+(** It should have length 1, just like contr_paths_contr0 *)
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 08628377f0..c6fcc24b6b 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -5,6 +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".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index ae17fb145d..64c7fd8eb1 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -5,6 +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".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -223,4 +224,4 @@ v = _) r,
     | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good"
     | [ |- ?G ] => fail 1 "bad" G
     end.
-    Fail rewrite concat_p_pp.
\ No newline at end of file
+    Fail rewrite concat_p_pp.
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index da140c9318..64dd8c304f 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -2,6 +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".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -1004,4 +1005,4 @@ Proof.
   Fail Timeout 1 Time rewrite !loops_functor_group.
   (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *)
   Timeout 1 do 3 rewrite loops_functor_group.
-Abort.
\ No newline at end of file
+Abort.
-- 
cgit v1.2.3


From 3602b909afc6eac0f150c9961a04b0bf50d8bbf0 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Fri, 10 Mar 2017 11:05:27 -0500
Subject: funind: Ignore missing info for current function

Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372)
"Anomaly: Not a valid information when defining mutual fixpoints that
are not mutual with Function".
---
 test-suite/bugs/closed/5372.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/5372.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5372.v b/test-suite/bugs/closed/5372.v
new file mode 100644
index 0000000000..2dc78d4c7f
--- /dev/null
+++ b/test-suite/bugs/closed/5372.v
@@ -0,0 +1,7 @@
+(* coq bug 5372: https://coq.inria.fr/bugs/show_bug.cgi?id=5372 *)
+Function odd (n:nat) :=
+  match n with
+  | 0 => false
+  | S n => true
+  end
+with even (n:nat) := false.
-- 
cgit v1.2.3


From b1656b1f10501b34ae6a7e147f550710b935e54b Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Wed, 22 Mar 2017 20:35:38 -0400
Subject: Intern names bound in match patterns

Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345):
Cannot use names bound in matches inside Ltac definitions.
---
 test-suite/bugs/closed/5345.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/5345.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5345.v b/test-suite/bugs/closed/5345.v
new file mode 100644
index 0000000000..d8448f35db
--- /dev/null
+++ b/test-suite/bugs/closed/5345.v
@@ -0,0 +1,7 @@
+Ltac break_tuple :=
+  match goal with
+  | [ H: context[match ?a with | pair n m => _ end] |- _ ] =>
+    let n := fresh n in
+    let m := fresh m in
+    destruct a as [n m]
+  end.
-- 
cgit v1.2.3