diff options
Diffstat (limited to 'src/hls/Verilog.v')
| -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. |