diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-24 16:57:12 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-24 16:57:12 -0400 |
| commit | 7a100fc8ea85cc1d93b5dcef2016b1db5eca631e (patch) | |
| tree | 392427ad9599cfe091632464d4bc1c092b84c71e /src/Util/Tuple.v | |
| parent | 61dd34005e6ccea1ac806f8c27b72166901ae6ea (diff) | |
Fix for Coq 8.4
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 48e51fc38..ad40b5e90 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -131,7 +131,7 @@ Local Ltac Equivalence_fieldwise'_t := | [ |- Equivalence _ ] => constructor end; induction n as [|? IHn]; [solve [auto]|]; - simpl; constructor; repeat intro; intuition eauto. + simpl; constructor; repeat intro; repeat intuition eauto. Section Equivalence. Context {A} {R:relation A}. |