From ec3eb238ea6f74bac4affb4b3744ea2ab700774c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 16 Dec 2018 19:19:28 +0100
Subject: [PATCH] A Coq bug printing spurious parentheses has been fixed.

See Coq PR#9214.
---
 tests/list_reverse.8.10.ref | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 tests/list_reverse.8.10.ref

diff --git a/tests/list_reverse.8.10.ref b/tests/list_reverse.8.10.ref
new file mode 100644
index 000000000..9440658db
--- /dev/null
+++ b/tests/list_reverse.8.10.ref
@@ -0,0 +1,33 @@
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  hd, acc : val
+  xs, ys : list val
+  Φ : val → iPropI Σ
+  ============================
+  "Hxs" : is_list hd xs
+  "Hys" : is_list acc ys
+  "HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
+  --------------------------------------∗
+  WP rev hd acc [{ v, Φ v }]
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  acc : val
+  ys : list val
+  Φ : val → iPropI Σ
+  ============================
+  "Hys" : is_list acc ys
+  "HΦ" : ∀ w : val, is_list w ys -∗ Φ w
+  --------------------------------------∗
+  WP match: InjLV #() with
+       InjL <> => acc
+     | InjR "l" =>
+       let: "tmp1" := Fst ! "l" in
+       let: "tmp2" := Snd ! "l" in
+       "l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
+     end [{ v, Φ v }]
+  
-- 
GitLab