diff options
| author | Jasper Hugunin | 2020-12-15 19:02:03 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2020-12-15 19:02:03 -0800 |
| commit | b987bced399decd3b4247e2b4bb716d36846ee68 (patch) | |
| tree | 4382b14c83c0011bb4d659090ac1ed79963ddd9f /theories | |
| parent | 96ad23e59418798fc5960940291ab5ea8b6330b4 (diff) | |
Modify QArith/Qreduction.v to compile with -mangle-names
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/QArith/Qreduction.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 533c675415..e94ae1e789 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -129,19 +129,19 @@ Qed. Add Morphism Qplus' with signature (Qeq ==> Qeq ==> Qeq) as Qplus'_comp. Proof. - intros; unfold Qplus'. + intros ? ? H ? ? H0; unfold Qplus'. rewrite H, H0; auto with qarith. Qed. Add Morphism Qmult' with signature (Qeq ==> Qeq ==> Qeq) as Qmult'_comp. Proof. - intros; unfold Qmult'. + intros ? ? H ? ? H0; unfold Qmult'. rewrite H, H0; auto with qarith. Qed. Add Morphism Qminus' with signature (Qeq ==> Qeq ==> Qeq) as Qminus'_comp. Proof. - intros; unfold Qminus'. + intros ? ? H ? ? H0; unfold Qminus'. rewrite H, H0; auto with qarith. Qed. |