From e2fe373a1947206746dd43afe6c9815c69453def Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 28 Nov 2018 00:47:10 +0100
Subject: [build] Test tests in Travis, use coqc for tests.

`coqtop -batch` is an oxymoron, in prevision for upstream changes use
`coqc`.

We also call `make test` in Travis as to make CI more robust.
---
 tests/example1.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tests/example1.v')

diff --git a/tests/example1.v b/tests/example1.v
index 1b26aad824..023791050f 100644
--- a/tests/example1.v
+++ b/tests/example1.v
@@ -24,3 +24,4 @@ Goal forall n m, n + m = 0 -> n = 0.
 Proof.
 refine (fun () => '(fun n m H => _)).
 let t := get_hyp_by_name @H in Message.print (Message.of_constr t).
+Abort.
-- 
cgit v1.2.3