diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-04 14:35:43 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-04-04 16:05:55 -0400 |
| commit | 331fe3fcfb27d87dcfb0585ced3c051f19aaedf2 (patch) | |
| tree | a9af1a7f8bba3fb1f6e7d1610ca1553f5e5f23c2 /src/Util/Tuple.v | |
| parent | 6cba3c4e0572e9d917d3578c39f4f85cd3799b54 (diff) | |
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).
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 16 |
1 files changed, 8 insertions, 8 deletions
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} _ _ _. |