From 944722bb1496ca6bb7c22091ea39a65100cd04af Mon Sep 17 00:00:00 2001
From: "Yves Bertot (he)" <yves.bertot@inria.fr>
Date: Wed, 20 Sep 2023 15:39:26 +0200
Subject: [PATCH] adds a warning concerning the suitability of this example for
 JsCoq

---
 slides3.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/slides3.v b/slides3.v
index 156ca74..7ce94be 100644
--- a/slides3.v
+++ b/slides3.v
@@ -1,3 +1,5 @@
+(* Warning: the last lines of this file are unsuitable for use in JsCoq,
+  which does not provide Coquelicot or Interval *)
 Require Import ZArith Lia.
 
 Open Scope Z_scope.
-- 
GitLab