Skip to content
Snippets Groups Projects
Commit c8887f48 authored by Hai Dang's avatar Hai Dang
Browse files

bump gpfsl

parent 2d7f1fe3
No related branches found
No related tags found
No related merge requests found
Pipeline #14303 passed
...@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"] ...@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [ depends: [
"coq-gpfsl" { (= "dev.2019-01-30.2.6a0acfb2") | (= "dev") } "coq-gpfsl" { (= "dev.2019-01-31.0.5495b101") | (= "dev") }
] ]
...@@ -4,7 +4,7 @@ From iris.program_logic Require Import weakestpre. ...@@ -4,7 +4,7 @@ From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.bi Require Import fractional. From iris.bi Require Import fractional.
From iris.algebra Require Import excl csum frac auth. From iris.algebra Require Import excl csum frac auth.
From lrust.lang Require Import lang proofmode notation new_delete. From lrust.lang Require Import proofmode notation new_delete.
Set Default Proof Using "Type". Set Default Proof Using "Type".
(* JH: while working on Arc, I think figured that the "weak count (* JH: while working on Arc, I think figured that the "weak count
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment