diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-20 10:29:40 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-20 10:38:28 -0400 |
| commit | a1113958bfbc1ccbbe76be831bf36c616ef74e93 (patch) | |
| tree | 60c131ac21cc5ca60bbe278084a65b4aee08c147 /src/Util | |
| parent | 977d76eac55aa34799039cc6a757efe65e1e7564 (diff) | |
Variosu 8.5 fixes
- nsatz/field seem to do less unfolding (need eauto with field_nonzero
more)
- intuition doesn't destruct things (need dintuition (8.5 only) or
manual destruct)
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/Tuple.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index de1af2a95..6802a86c3 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -66,8 +66,9 @@ Defined. Global Instance Equivalence_fieldwise' {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}: Equivalence (fieldwise' n R). Proof. - induction n; [solve [auto]|]. - simpl; constructor; repeat intro; intuition eauto. + induction n as [|? IHn]; [solve [auto]|]. + (* could use [dintuition] in 8.5 only, and remove the [destruct] *) + destruct IHn, R_equiv; simpl; constructor; repeat intro; intuition eauto. Qed. Global Instance Equivalence_fieldwise {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}: @@ -77,4 +78,4 @@ Proof. Qed. Arguments fieldwise' {A B n} _ _ _. -Arguments fieldwise {A B n} _ _ _.
\ No newline at end of file +Arguments fieldwise {A B n} _ _ _. |