diff options
| author | Jasper Hugunin | 2020-09-09 10:41:35 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | 2128f623d1d9f26b5791d65e95c8d624ac7e48b9 (patch) | |
| tree | 4ee6dd5d20b592aa4963c4f94f64e9913d0c0bea | |
| parent | 6b677ba003748f6222539a083e9de7d47a60c373 (diff) | |
Modify Numbers/Natural/Abstract/NDiv.v to compile with -mangle-names
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDiv.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index 9c50d5ca58..bb2f32935f 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -39,15 +39,15 @@ Qed. Theorem div_mod_unique : forall b q1 q2 r1 r2, r1<b -> r2<b -> b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2. -Proof. intros. apply div_mod_unique with b; auto'. Qed. +Proof. intros b q1 q2 r1 r2 ? ? ?. apply div_mod_unique with b; auto'. Qed. Theorem div_unique: forall a b q r, r<b -> a == b*q + r -> q == a/b. -Proof. intros; apply div_unique with r; auto'. Qed. +Proof. intros a b q r ? ?; apply div_unique with r; auto'. Qed. Theorem mod_unique: forall a b q r, r<b -> a == b*q + r -> r == a mod b. -Proof. intros. apply mod_unique with q; auto'. Qed. +Proof. intros a b q r ? ?. apply mod_unique with q; auto'. Qed. Theorem div_unique_exact: forall a b q, b~=0 -> a == b*q -> q == a/b. Proof. intros. apply div_unique_exact; auto'. Qed. |