From 450bda69837b02c20d2fb391bbe7827d1becaac4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 14 Jul 2020 16:08:58 +0100 Subject: Change name to Vericert --- src/verilog/Array.v | 2 +- src/verilog/AssocMap.v | 4 ++-- src/verilog/HTL.v | 6 +++--- src/verilog/PrintHTL.ml | 4 ++-- src/verilog/PrintVerilog.ml | 4 ++-- src/verilog/PrintVerilog.mli | 2 +- src/verilog/Value.v | 4 ++-- src/verilog/ValueInt.v | 4 ++-- src/verilog/Verilog.v | 4 ++-- 9 files changed, 17 insertions(+), 17 deletions(-) (limited to 'src/verilog') 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 * * This program is free software: you can redistribute it and/or modify @@ -16,7 +16,7 @@ * along with this program. If not, see . *) -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 * * 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 * * 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 * * 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 * * 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 * * 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 * * 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 * * 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. -- cgit