From 9ac6592338ed5f540823e77c8cc0639cbdc39f96 Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Wed, 22 Aug 2018 12:03:31 +0200
Subject: [PATCH] Adapt simple regression test in Coq

---
 testcases/regression/certificate_AdditionSimple.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/testcases/regression/certificate_AdditionSimple.v b/testcases/regression/certificate_AdditionSimple.v
index 601c025e..418ef984 100644
--- a/testcases/regression/certificate_AdditionSimple.v
+++ b/testcases/regression/certificate_AdditionSimple.v
@@ -5,8 +5,9 @@ Definition e3 :expr Q := Binop Plus C12 u0.
 Definition Rete3 := Ret e3.
 
 
-Definition defVars_additionSimple :(nat -> option mType) := fun n =>
-if n =? 0 then Some M64 else None.
+Definition defVars_additionSimple :(FloverMap.t mType) :=
+  FloverMap.add (Var Q 0) M64 (FloverMap.empty mType).
+
 Definition thePrecondition_additionSimple:precond := fun (n:nat) =>
 if n =? 0 then ( (-100)#(1), (100)#(1)) else (0#1,0#1).
 
-- 
GitLab