Skip to content
Snippets Groups Projects
Commit 47f94239 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix build on old Coq

parent 153bc7bd
No related branches found
No related tags found
No related merge requests found
...@@ -71,9 +71,9 @@ ...@@ -71,9 +71,9 @@
"wp_load_fail" "wp_load_fail"
: string : string
The command has indeed failed with message: The command has indeed failed with message:
Tactic failure: wp_load: cannot find 'Load' in (Fork Skip). Tactic failure: wp_load: cannot find 'Load' in (Fork #()).
The command has indeed failed with message: The command has indeed failed with message:
Tactic failure: wp_load: cannot find 'Load' in (Fork Skip). Tactic failure: wp_load: cannot find 'Load' in (Fork #()).
"wp_load_no_ptsto" "wp_load_no_ptsto"
: string : string
The command has indeed failed with message: The command has indeed failed with message:
...@@ -81,9 +81,9 @@ Tactic failure: wp_load: cannot find l ↦ ?. ...@@ -81,9 +81,9 @@ Tactic failure: wp_load: cannot find l ↦ ?.
"wp_store_fail" "wp_store_fail"
: string : string
The command has indeed failed with message: The command has indeed failed with message:
Tactic failure: wp_store: cannot find 'Store' in (Fork Skip). Tactic failure: wp_store: cannot find 'Store' in (Fork #()).
The command has indeed failed with message: The command has indeed failed with message:
Tactic failure: wp_store: cannot find 'Store' in (Fork Skip). Tactic failure: wp_store: cannot find 'Store' in (Fork #()).
"wp_store_no_ptsto" "wp_store_no_ptsto"
: string : string
The command has indeed failed with message: The command has indeed failed with message:
......
...@@ -151,10 +151,10 @@ Section tests. ...@@ -151,10 +151,10 @@ Section tests.
Check "wp_load_fail". Check "wp_load_fail".
Lemma wp_load_fail : Lemma wp_load_fail :
WP Fork Skip {{ _, True }}. WP Fork #() {{ _, True }}.
Proof. Fail wp_load. Abort. Proof. Fail wp_load. Abort.
Lemma twp_load_fail : Lemma twp_load_fail :
WP Fork Skip [{ _, True }]. WP Fork #() [{ _, True }].
Proof. Fail wp_load. Abort. Proof. Fail wp_load. Abort.
Check "wp_load_no_ptsto". Check "wp_load_no_ptsto".
Lemma wp_load_fail_no_ptsto (l : loc) : Lemma wp_load_fail_no_ptsto (l : loc) :
...@@ -163,10 +163,10 @@ Section tests. ...@@ -163,10 +163,10 @@ Section tests.
Check "wp_store_fail". Check "wp_store_fail".
Lemma wp_store_fail : Lemma wp_store_fail :
WP Fork Skip {{ _, True }}. WP Fork #() {{ _, True }}.
Proof. Fail wp_store. Abort. Proof. Fail wp_store. Abort.
Lemma twp_store_fail : Lemma twp_store_fail :
WP Fork Skip [{ _, True }]. WP Fork #() [{ _, True }].
Proof. Fail wp_store. Abort. Proof. Fail wp_store. Abort.
Check "wp_store_no_ptsto". Check "wp_store_no_ptsto".
Lemma wp_store_fail_no_ptsto (l : loc) : Lemma wp_store_fail_no_ptsto (l : loc) :
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment