diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-10 15:04:32 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-10 15:04:32 -0400 |
| commit | 6ee6d5242d8caab769bd60ee4d44efe41add8bda (patch) | |
| tree | aa309b28c4c7279b113a55dcbe7b8fd9b03801cc /src/Util/ZUtil/Hints | |
| parent | f2ddb29e6ab3c2390b2bb78260c082e52616ff0a (diff) | |
Add Z.pow_mod_Proper
Diffstat (limited to 'src/Util/ZUtil/Hints')
| -rw-r--r-- | src/Util/ZUtil/Hints/Core.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Hints/Core.v b/src/Util/ZUtil/Hints/Core.v index dff4b7b26..1739e72af 100644 --- a/src/Util/ZUtil/Hints/Core.v +++ b/src/Util/ZUtil/Hints/Core.v @@ -1,6 +1,7 @@ (** * Declaration of Hint Databases with lemmas about ℤ from the standard library *) Require Import Coq.micromega.Psatz Coq.omega.Omega. Require Import Coq.ZArith.ZArith. +(* Should we [Require Import Coq.ZArith.Zhints.]? *) Hint Extern 1 => lia : lia. Hint Extern 1 => lra : lra. |