From a1113958bfbc1ccbbe76be831bf36c616ef74e93 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 20 Jun 2016 10:29:40 -0400 Subject: 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) --- src/Util/Tuple.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/Util') 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} _ _ _. -- cgit v1.2.3