diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-03-19 15:09:59 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-03-19 15:09:59 +0000 |
| commit | 83e716e65a3d497387e6bf8f33de29fff3bd269d (patch) | |
| tree | 46a96b9b6e3038adb4d866b9a8e886e96ec247b7 /src/Verilog | |
| parent | 2217a79966ec6a3ff84ba9da4cdb9d511c1c8b23 (diff) | |
| download | vericert-83e716e65a3d497387e6bf8f33de29fff3bd269d.tar.gz vericert-83e716e65a3d497387e6bf8f33de29fff3bd269d.zip | |
Update names of directories
Diffstat (limited to 'src/Verilog')
| -rw-r--r-- | src/Verilog/VerilogAST.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Verilog/VerilogAST.v b/src/Verilog/VerilogAST.v index 5886652..8bb8ba8 100644 --- a/src/Verilog/VerilogAST.v +++ b/src/Verilog/VerilogAST.v @@ -22,7 +22,8 @@ Structures.OrderedTypeEx FSets.FMapList Program.Basics PeanoNat. -From CoqUp.Common Require Import Helper Tactics Show. + +From coqup.common Require Import Helper Tactics Show. Import ListNotations. @@ -32,8 +33,7 @@ Inductive value : Type := | VBool (b : bool) | VArray (l : list value). -Inductive literal : Type := -| LitArray (l : list bool). +Inductive literal : Type := LitArray (l : list bool). Definition cons_value (a b : value) : value := match a, b with |