diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-02-18 15:40:37 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-02-18 15:40:37 -0500 |
| commit | 6ad369b1c322c7edc249521149a45b433bc9018e (patch) | |
| tree | 0a2849096454412bff4a79982be1dbc1b77fa8a9 /src | |
| parent | de7dbd6bb083b008280d1c26ba3bbef39d720e50 (diff) | |
Add some imports to experiments
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index d6dffe3ce..44beaa3ee 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -1,5 +1,6 @@ (* Following http://adam.chlipala.net/theses/andreser.pdf chapter 3 *) Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. +Require Import Coq.Strings.String. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. Require Import Coq.derive.Derive. @@ -13,6 +14,7 @@ Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.Tactics.RunTacticAsConstr. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Option. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope Z_scope. |