diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-03-15 19:40:16 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-15 19:40:16 +0000 |
| commit | 280b80298e76ef99b8e1908ec32afb4c700c60ee (patch) | |
| tree | 4d678ea173075d3919f022c092de913774a5b7a3 | |
| parent | 2ccfaa9cbb2b45adb7368afd329f743a9b10b04b (diff) | |
| download | vericert-280b80298e76ef99b8e1908ec32afb4c700c60ee.tar.gz vericert-280b80298e76ef99b8e1908ec32afb4c700c60ee.zip | |
Move implicit args
| -rw-r--r-- | src/hls/Verilog.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 1e4be92..a9ec5a1 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -17,6 +17,8 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) +Set Implicit Arguments. + Require Import Coq.Structures.OrderedTypeEx. Require Import Coq.FSets.FMapPositive. Require Import Coq.Program.Basics. @@ -42,8 +44,6 @@ Import ListNotations. Local Open Scope assocmap. -Set Implicit Arguments. - Definition reg : Type := positive. Definition node : Type := positive. Definition szreg : Type := reg * nat. |