diff options
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 5a2ea19a4..f71807fff 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -5,6 +5,7 @@ Require Import Crypto.Util.Notations. Require Coq.Numbers.Natural.Peano.NPeano. Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope. Require Crypto.Tactics.Algebra_syntax.Nsatz. +Require Export Crypto.Util.FixCoqMistakes. Module Import ModuloCoq8485. Import NPeano Nat. |