diff options
| author | Frédéric Besson | 2020-04-01 11:43:00 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2020-04-01 11:43:00 +0200 |
| commit | 288a97e465048bc47c7d5e91e14bfbc33819e689 (patch) | |
| tree | 1b6afa192518791fe2ae47e3fb4d3033070f4a65 /theories/ZArith | |
| parent | 402e37a405e4085365fdcbdc959fe00d2c340da2 (diff) | |
[micromega] use Coqlib.lib_ref to get Coq constants.
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/BinInt.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 0b3656f586..78b26c83ea 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -44,6 +44,7 @@ Register succ as num.Z.succ. Register pred as num.Z.pred. Register sub as num.Z.sub. Register mul as num.Z.mul. +Register pow as num.Z.pow. Register of_nat as num.Z.of_nat. (** When including property functors, only inline t eq zero one two *) |