Commit fd86b7bb authored by Ralf Jung's avatar Ralf Jung

do "Print Assumptions" outside of sections

parent 4206ef52
...@@ -6,7 +6,7 @@ buildjob: ...@@ -6,7 +6,7 @@ buildjob:
script: script:
- coqc -v - coqc -v
- 'time make -j8 TIMED=y 2>&1 | tee build-log.txt' - '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' - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
- make verify - make verify
only: only:
......
...@@ -59,7 +59,7 @@ End client. ...@@ -59,7 +59,7 @@ End client.
Section ClosedProofs. Section ClosedProofs.
Definition Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ]. Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
Lemma client_adequate σ : adequate client σ (λ _, True). Lemma client_adequate σ : adequate client σ (λ _, True).
Proof. Proof.
...@@ -67,6 +67,6 @@ Proof. ...@@ -67,6 +67,6 @@ Proof.
apply (client_safe (nroot .@ "barrier")); auto with ndisj. apply (client_safe (nroot .@ "barrier")); auto with ndisj.
Qed. Qed.
Print Assumptions client_adequate.
End ClosedProofs. End ClosedProofs.
Print Assumptions client_adequate.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment