diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 21:52:57 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 21:52:57 -0400 |
| commit | cf71d9060d90d3d25e899eb1d8473681152e4695 (patch) | |
| tree | c99bec19430cd4b4104621a32f02c0f4aa54b9be /src/Util/PartiallyReifiedProp.v | |
| parent | 9d638523e5e393d3c739cc7b24b56f366fc851bb (diff) | |
Fix for 8.5 build?
Diffstat (limited to 'src/Util/PartiallyReifiedProp.v')
| -rw-r--r-- | src/Util/PartiallyReifiedProp.v | 3 |
1 files changed, 2 insertions, 1 deletions
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 |