Commit 7b03d0b3 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix build on master Coq by fixing Require order.

parent da7641e9
Pipeline #19780 passed with stage
in 18 minutes and 23 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-07-01.1.6e79f000") | (= "dev") }
"coq-iris" { (= "dev.2019-09-19.0.ca3f9d11") | (= "dev") }
]
From iris.bi.lib Require Import fractional.
From iris.algebra Require Import auth agree excl frac gmap gset.
From iris.base_logic.lib Require Import cancelable_invariants auth saved_prop.
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock.
From iris.base_logic.lib Require Import cancelable_invariants auth saved_prop.
From iris.algebra Require Import auth agree excl frac gmap gset.
From iris.bi.lib Require Import fractional.
Inductive lockstate :=
| Locked
......
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