From 331fe3fcfb27d87dcfb0585ced3c051f19aaedf2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Apr 2017 14:35:43 -0400 Subject: Add [Proof using] to most proofs This closes #146 and makes `make quick` faster. The changes were generated by adding [Global Set Suggest Proof Using.] to GlobalSettings.v, and then following [the instructions for a script I wrote](https://github.com/JasonGross/coq-tools#proof-using-helper). --- src/Util/Tuple.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 03cb4492b..615410f2a 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -486,22 +486,22 @@ Local Ltac Equivalence_fieldwise'_t := Section Equivalence. Context {A} {R:relation A}. Global Instance Reflexive_fieldwise' {R_Reflexive:Reflexive R} {n:nat} : Reflexive (fieldwise' n R) | 5. - Proof. Equivalence_fieldwise'_t. Qed. + Proof using Type. Equivalence_fieldwise'_t. Qed. Global Instance Symmetric_fieldwise' {R_Symmetric:Symmetric R} {n:nat} : Symmetric (fieldwise' n R) | 5. - Proof. Equivalence_fieldwise'_t. Qed. + Proof using Type. Equivalence_fieldwise'_t. Qed. Global Instance Transitive_fieldwise' {R_Transitive:Transitive R} {n:nat} : Transitive (fieldwise' n R) | 5. - Proof. Equivalence_fieldwise'_t. Qed. + Proof using Type. Equivalence_fieldwise'_t. Qed. Global Instance Equivalence_fieldwise' {R_equiv:Equivalence R} {n:nat} : Equivalence (fieldwise' n R). - Proof. constructor; exact _. Qed. + Proof using Type. constructor; exact _. Qed. Global Instance Reflexive_fieldwise {R_Reflexive:Reflexive R} {n:nat} : Reflexive (fieldwise n R) | 5. - Proof. destruct n; (repeat constructor || exact _). Qed. + Proof using Type. destruct n; (repeat constructor || exact _). Qed. Global Instance Symmetric_fieldwise {R_Symmetric:Symmetric R} {n:nat} : Symmetric (fieldwise n R) | 5. - Proof. destruct n; (repeat constructor || exact _). Qed. + Proof using Type. destruct n; (repeat constructor || exact _). Qed. Global Instance Transitive_fieldwise {R_Transitive:Transitive R} {n:nat} : Transitive (fieldwise n R) | 5. - Proof. destruct n; (repeat constructor || exact _). Qed. + Proof using Type. destruct n; (repeat constructor || exact _). Qed. Global Instance Equivalence_fieldwise {R_equiv:Equivalence R} {n:nat} : Equivalence (fieldwise n R). - Proof. constructor; exact _. Qed. + Proof using Type. constructor; exact _. Qed. End Equivalence. Arguments fieldwise' {A B n} _ _ _. -- cgit v1.2.3