diff --git a/slides3.v b/slides3.v
index 156ca74fe9e724cecc0400f94fe787bfcb131d6c..7ce94bed693a0174e756c18cb4fbc6cd9471e5b8 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.