From f4ecdfa82e8262fa353dba3f9f1acbd6adbfecc0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 19 Jul 2016 15:15:13 +0200
Subject: [PATCH] make list_reverse compile
---
tests/list_reverse.v | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 647aa6749..804de44d6 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -16,13 +16,13 @@ Fixpoint is_list (hd : val) (xs : list val) : iProp :=
Definition rev : val :=
rec: "rev" "hd" "acc" :=
- match: "hd" with
- NONE => "acc"
+ match: '"hd" with
+ NONE => '"acc"
| SOME "l" =>
- let: "tmp1" := Fst !"l" in
- let: "tmp2" := Snd !"l" in
- "l" <- ("tmp1", "acc");;
- "rev" "tmp2" "hd"
+ let: "tmp1" := Fst !'"l" in
+ let: "tmp2" := Snd !'"l" in
+ '"l" <- ('"tmp1", '"acc");;
+ '"rev" '"tmp2" '"hd"
end.
Global Opaque rev.
--
GitLab