diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-31 19:17:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-31 19:17:57 +0200 |
| commit | 7f4cb6a3a83b571f5af12bb69255d4b492ef8311 (patch) | |
| tree | 2ddd4c3185320f5e2b4c9bb39108ed79b057f8f6 | |
| parent | 765510929b2255d9c56fcdfce4a3ea555b07b340 (diff) | |
Fixing test-suite.
| -rw-r--r-- | test-suite/bugs/closed/3881.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_107.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index 7c3cc6b79..4408ab885 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 9a1da16bf..7c1ab8dc2 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. |