diff options
| author | Jasper Hugunin | 2020-08-25 13:11:43 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:32 -0700 |
| commit | 1a7dfd1bfce28a0ff20ba4ce58440d99bca3fbb3 (patch) | |
| tree | 0cb7a9e4d0ad7ebdebccf8fe75d0b583152829f7 | |
| parent | c16e4c23e6591aace243c5503ce70e99d3c0569d (diff) | |
Modify Numbers/NatInt/NZBase.v to compile with -mangle-names
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 8bc393bbad..e6eabd5b2c 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -74,7 +74,7 @@ Proof. intros z Base Step; revert Base; pattern z; apply bi_induction. - solve_proper. - intro; now apply bi_induction. -- intro; pose proof (Step n); tauto. +- intro n; pose proof (Step n); tauto. Qed. End CentralInduction. |