aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-05-15 22:35:51 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-05-18 10:41:13 +0200
commitab791c6dfa839e096e93cd9edf9e6bdb9ec93e57 (patch)
tree05373f846d63e5e0126b63b2353d763e41222d7c
parent8aebd0c751db55c0301518d8ed55b8ac7bccae27 (diff)
Removing option -no-native-compiler from test #3539 since this option is now
negated into -native-compiler.
-rw-r--r--test-suite/bugs/closed/3539.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3539.v b/test-suite/bugs/closed/3539.v
index c862965d4..d258bb31f 100644
--- a/test-suite/bugs/closed/3539.v
+++ b/test-suite/bugs/closed/3539.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-no-native-compiler") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
(* File reduced by coq-bug-finder from original input, then from 11678 lines to 11330 lines, then from 10721 lines to 9544 lines, then from 9549 lines to 794 lines, then from 810 lines to 785 lines, then from 628 lines to 246 lines, then from 220 lines to 89 lines, then from 80 lines to 47 lines *)
(* coqc version trunk (August 2014) compiled on Aug 22 2014 4:17:28 with OCaml 4.01.0
coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (a67cc6941434124465f20b14a1256f2ede31a60e) *)
@@ -63,4 +63,4 @@ x' : forall (_ : T1) (_ : T), T2
m : T3 (x' fst1 x2) (x' fst0 x2)
Unable to unify "?25 (@pair ?23 ?24 (fst ?27) (snd ?27))" with
"?25 ?27".
- *) \ No newline at end of file
+ *)