From 5e38184af1b99a307271f738329cd96cb364fc1d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Aug 2023 22:31:48 +0200
Subject: Update the Makefile and regenerate the test files

---
 tests/coq/misc/Paper.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'tests/coq/misc/Paper.v')

diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 0f854f31..175a523d 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -3,6 +3,8 @@
 Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
 Local Open Scope Primitives_scope.
 Module Paper.
 
-- 
cgit v1.2.3