diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-06-14 15:29:36 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-06-14 15:29:36 -0400 |
| commit | ff051043f926a15ed2575122791e1d7c57fe7ac1 (patch) | |
| tree | 32796809b1b4397c9913fd504715c931a92c1df9 /src/Util/NatUtil.v | |
| parent | 44a9f78bb082dbc5275f7d4ae07501dc7cba8a07 (diff) | |
| parent | 656f38ab96e18740df46868f31ac20814ffd6658 (diff) | |
Merge
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 59898be7a..bc2c8425b 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,4 +1,5 @@ Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. +Import Nat. Local Open Scope nat_scope. @@ -77,4 +78,3 @@ Proof. [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ]. Qed. - |