diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index dd46f17322ba82e2dac4b9607d569492d043cdf1..abef5df4be58b4c08bfa4dd015b04835d90fa0f5 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 79bf4c9a9b6f21197a10822c78c821c2902e7c34..dac3e09c35a59dce6faa957713e42acca4a7f0ff 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.