Commit 9db1d7a4 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix build on master Coq by fixing Require order.

parent db3fd5c0
Pipeline #19781 passed with stage
in 24 minutes and 4 seconds
......@@ -9,6 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [
"coq-iris" { (= "dev.2019-08-13.5.c1d6ef7f") | (= "dev") }
"coq-iris" { (= "dev.2019-09-19.0.ca3f9d11") | (= "dev") }
]
(** This file defines the basic points-to [↦] connectives for the Iron logic
instantiated with the heap_lang language. As a counter part to this, it defines
the state interpretation [heap_ctx]. *)
From iris.algebra Require Import excl frac_auth gmap agree gmultiset ufrac ufrac_auth.
From iris.base_logic.lib Require Export own.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iron.proofmode Require Export fracpred.
From iron.heap_lang Require Export lang.
From iris.algebra Require Import excl frac_auth gmap agree gmultiset ufrac ufrac_auth.
From iris.base_logic.lib Require Export own.
From iron.iron_logic Require Export weakestpre.
From iron.heap_lang Require Export lang.
Set Default Proof Using "Type".
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (agreeR valO)).
......
......@@ -6,8 +6,8 @@
* The crucial specification is in [par_spec]; [wp_par] is a convenient
* wrapper around this specification for use in other interactive proofs.
*)
From iron.heap_lang Require Export spawn.
From iron.heap_lang Require Import proofmode notation.
From iron.heap_lang Require Export spawn.
Set Default Proof Using "Type".
Import uPred.
......
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