From b70f1bcb1b51f2e2097694f9d99123df399341e9 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Wed, 22 May 2019 19:11:39 -0400
Subject: [PATCH] Revert spurious change to ref file.

---
 tests/proofmode.ref | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 35af41d6d..df2cc9712 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -118,7 +118,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   ============================
   "H1" : ⌜S (S (S x)) = y⌝
   --------------------------------------□
-  "H2" : ⌜1 + y = z⌝
+  "H2" : ⌜(1 + y)%nat = z⌝
   --------------------------------------∗
   ⌜S (S (S x)) = y⌝
   
-- 
GitLab