Change name to Vericert

9 files changed, 17 insertions, 17 deletions

diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index be06541..02b6d33 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -1,7 +1,7 @@
 Set Implicit Arguments.
 
 Require Import Lia.
-Require Import Coquplib.
+Require Import Vericertlib.
 From Coq Require Import Lists.List Datatypes.
 
 Import ListNotations.
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index c5cfa3f..8d8788a 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Import Coquplib ValueInt.
+From vericert Require Import Vericertlib ValueInt.
 From compcert Require Import Maps.
 
 Definition reg := positive.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index b3d1442..620ef14 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -17,8 +17,8 @@
  *)
 
 From Coq Require Import FSets.FMapPositive.
-From coqup Require Import Coquplib ValueInt AssocMap Array.
-From coqup Require Verilog.
+From vericert Require Import Vericertlib ValueInt AssocMap Array.
+From vericert Require Verilog.
 From compcert Require Events Globalenvs Smallstep Integers Values.
 From compcert Require Import Maps.
 
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
index 0bdba51..44f8b01 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/verilog/PrintHTL.ml
@@ -1,5 +1,5 @@
 (* -*- mode: tuareg -*-
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -27,7 +27,7 @@ open AST
 open HTL
 open PrintAST
 open PrintVerilog
-open CoqupClflags
+open VericertClflags
 
 let pstr pp = fprintf pp "%s"
 
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 5265c97..f348ee6 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -1,5 +1,5 @@
 (* -*- mode: tuareg -*-
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -26,7 +26,7 @@ open Clflags
 
 open Printf
 
-open CoqupClflags
+open VericertClflags
 
 let concat = String.concat ""
 
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 62bf63f..47af3ef 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -1,5 +1,5 @@
 (* 
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index af2b822..41a41b4 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -21,7 +21,7 @@ From bbv Require Import Word.
 From bbv Require HexNotation WordScope.
 From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
 From compcert Require Import lib.Integers common.Values.
-From coqup Require Import Coquplib.
+From vericert Require Import Vericertlib.
 (* end hide *)
 
 (** * Value
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v
index f0f6de6..c7f69a1 100644
--- a/src/verilog/ValueInt.v
+++ b/src/verilog/ValueInt.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -21,7 +21,7 @@ From bbv Require Import Word.
 From bbv Require HexNotation WordScope.
 From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
 From compcert Require Import lib.Integers common.Values.
-From coqup Require Import Coquplib.
+From vericert Require Import Vericertlib.
 (* end hide *)
 
 (** * Value
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 321bdc2..3b0dd0a 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -29,7 +29,7 @@ Require Import Lia.
 
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.ValueInt AssocMap Array.
+From vericert Require Import common.Vericertlib common.Show verilog.ValueInt AssocMap Array.
 From compcert Require Events.
 From compcert Require Import Integers Errors Smallstep Globalenvs.