From 7f4cb6a3a83b571f5af12bb69255d4b492ef8311 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 31 Mar 2015 19:17:57 +0200
Subject: Fixing test-suite.

---
 test-suite/bugs/closed/3881.v         | 2 +-
 test-suite/bugs/closed/HoTT_coq_107.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v
index 7c3cc6b791..4408ab885d 100644
--- a/test-suite/bugs/closed/3881.v
+++ b/test-suite/bugs/closed/3881.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* -*- coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 2236 lines to 1877 lines, then from 1652 lines to 160 lines, then from 102 lines to 34 lines *)
 (* coqc version trunk (December 2014) compiled on Dec 23 2014 22:6:43 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *)
diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v
index 9a1da16bf6..7c1ab8dc2c 100644
--- a/test-suite/bugs/closed/HoTT_coq_107.v
+++ b/test-suite/bugs/closed/HoTT_coq_107.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-nois" "-emacs") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *)
 (* 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.
-- 
cgit v1.2.3


From a297f5cbeb5f76cae593a0778605ce9050e9d1c5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 1 Apr 2015 12:31:59 +0200
Subject: Fixing test-suite.

---
 test-suite/success/Injection.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 6a48824438..25e464d677 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -1,3 +1,5 @@
+Require Eqdep_dec.
+
 (* Check the behaviour of Injection *)
 
 (* Check that Injection tries Intro until *)
-- 
cgit v1.2.3


From ee9d9415c518e703a10a53acfdea8627547565fe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 6 Apr 2015 09:04:40 +0200
Subject: Test for bug #3815.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3815.v b/test-suite/bugs/closed/3815.v
new file mode 100644
index 0000000000..5fb4839847
--- /dev/null
+++ b/test-suite/bugs/closed/3815.v
@@ -0,0 +1,9 @@
+Require Import Setoid Coq.Program.Basics.
+Global Open Scope program_scope.
+Axiom foo : forall A (f : A -> A), f ∘ f = f.
+Require Import Coq.Program.Combinators.
+Hint Rewrite foo.
+Theorem t {A B C D} (f : A -> A) (g : B -> C) (h : C -> D)
+: f ∘ f = f.
+Proof.
+  rewrite_strat topdown (hints core).
-- 
cgit v1.2.3