From fd86b7bb789277fe7cb131689069e83216c0aad4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 19 Aug 2016 13:54:35 +0200
Subject: [PATCH] do "Print Assumptions" outside of sections

---
 .gitlab-ci.yml         | 2 +-
 tests/barrier_client.v | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index dd46f1732..abef5df4b 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -6,7 +6,7 @@ buildjob:
   script:
   - coqc -v
   - 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
-  - 'grep Axiom build-log.txt && exit 1'
+  - 'fgrep Axiom build-log.txt && exit 1'
   - 'cat build-log.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
   - make verify
   only:
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 79bf4c9a9..dac3e09c3 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -59,7 +59,7 @@ End client.
 
 Section ClosedProofs.
 
-Definition Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
+Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
 
 Lemma client_adequate σ : adequate client σ (λ _, True).
 Proof.
@@ -67,6 +67,6 @@ Proof.
   apply (client_safe (nroot .@ "barrier")); auto with ndisj.
 Qed.
 
-Print Assumptions client_adequate.
-
 End ClosedProofs.
+
+Print Assumptions client_adequate.
-- 
GitLab