From 6328da7d2ce8e2c1f378c941f25739f60d55570b Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 21 May 2019 12:42:09 +0100
Subject: Coq: remove premature unfolding of local definitions

---
 lib/coq/Sail2_values.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 8323ccfd..61e2c6a4 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1126,7 +1126,7 @@ Ltac extract_properties :=
     let x := fresh "x" in
     let Hx := fresh "Hx" in
     destruct X as [x Hx] in *;
-    change (projT1 (existT _ x Hx)) with x in *; unfold H in * end;
+    change (projT1 (existT _ x Hx)) with x in * end;
   (* Properties in the goal *)
   repeat match goal with |- context [projT1 ?X] =>
     let x := fresh "x" in
-- 
cgit v1.2.3