diff options
| author | Pierre Letouzey | 2015-04-09 14:46:37 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2015-04-09 14:46:37 +0200 |
| commit | 429f493997e34bfaac930c68bf6b267a5b9640ee (patch) | |
| tree | 28f15d0aeff2ce899a312f31e10fe2030b2dd813 /test-suite | |
| parent | aeec29a177e8f1c89996c0449e4cd81ca3ca4377 (diff) | |
| parent | eaa3f9719d6190ba92ce55816f11c70b30434309 (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/3815.v | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3881.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_107.v | 2 | ||||
| -rw-r--r-- | test-suite/success/Injection.v | 2 |
4 files changed, 13 insertions, 2 deletions
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). 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. 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 *) |