From cf71d9060d90d3d25e899eb1d8473681152e4695 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 30 Oct 2016 21:52:57 -0400
Subject: Fix for 8.5 build?

---
 src/Util/PartiallyReifiedProp.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/Util/PartiallyReifiedProp.v')

diff --git a/src/Util/PartiallyReifiedProp.v b/src/Util/PartiallyReifiedProp.v
index c950b0971..b10d550ae 100644
--- a/src/Util/PartiallyReifiedProp.v
+++ b/src/Util/PartiallyReifiedProp.v
@@ -3,6 +3,7 @@
     computationally reduce things like [True /\ True], but can still
     express equality of types. *)
 Require Import Coq.Setoids.Setoid.
+Require Import Coq.Program.Tactics.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.
 
@@ -94,7 +95,7 @@ Section rel.
             || intuition try congruence
             || (exists eq_refl)
             || eauto
-            || subst
+            || (subst * )
             || apply conj
             || destruct_head' ex
             || solve [ apply reflexivity
-- 
cgit v1.2.3