5 files changed, 18 insertions, 19 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 1cc30c7..8245a06 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.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
@@ -19,7 +19,7 @@
 From compcert Require Import Maps.
 From compcert Require Errors Globalenvs Integers.
 From compcert Require Import AST RTL.
-From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt Statemonad.
+From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad.
 
 Hint Resolve AssocMap.gempty : htlh.
 Hint Resolve AssocMap.gso : htlh.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index dd1d967..ddf8c3a 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.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
@@ -18,8 +18,8 @@
 
 From compcert Require RTL Registers AST.
 From compcert Require Import Integers Globalenvs Memory Linking.
-From coqup Require Import Coquplib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra.
-From coqup Require HTL Verilog.
+From vericert Require Import Vericertlib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra.
+From vericert Require HTL Verilog.
 
 Require Import Lia.
 
@@ -708,13 +708,12 @@ Section CORRECTNESS.
             Admitted.
 
   Lemma eval_cond_correct :
-    forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa,
-      translate_condition cond args s1 = OK c s' i ->
-      Op.eval_condition
-        cond
-        (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args)
-        m = Some b ->
-      Verilog.expr_runp f asr asa c (boolToValue b).
+    exists v' : value,
+      Verilog.expr_runp f' asr asa e v' /\
+      val_value_lessdef
+        (Values.Val.of_optbool
+           (Op.eval_condition cond
+                              (map (fun r : positive => Registers.Regmap.get r rs) args) m)) v'
   Admitted.
 
   (** The proof of semantic preservation for the translation of instructions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 71fb618..93d5612 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.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
@@ -18,7 +18,7 @@
 
 From compcert Require RTL Op Maps Errors.
 From compcert Require Import Maps Integers.
-From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap.
+From vericert Require Import Vericertlib Verilog ValueInt HTL HTLgen AssocMap.
 Require Import Lia.
 
 Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index f5d5fa7..a0be0fa 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.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
@@ -19,7 +19,7 @@
 From compcert Require Import Maps.
 From compcert Require Errors.
 From compcert Require Import AST.
-From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt.
+From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt.
 
 Definition transl_list_fun (a : node * Verilog.stmnt) :=
   let (n, stmnt) := a in
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index 5b467a7..9abbd4b 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.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 compcert Require Import Smallstep Linking Integers Globalenvs.
-From coqup Require HTL.
-From coqup Require Import Coquplib Veriloggen Verilog ValueInt AssocMap.
+From vericert Require HTL.
+From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap.
 Require Import Lia.
 
 Local Open Scope assocmap.