From 2a511a7edb9ebecad52f094111abd9c0c4187f7c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 9 May 2022 14:13:25 +0200
Subject: [PATCH] fix warning

---
 elpi-builtin.elpi | 4 ++--
 tests/test_API.v  | 4 ++--
 tests/test_API2.v | 8 ++++----
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/elpi-builtin.elpi b/elpi-builtin.elpi
index f6750fae4..c3dc18f8f 100644
--- a/elpi-builtin.elpi
+++ b/elpi-builtin.elpi
@@ -353,8 +353,8 @@ external type constant any -> variadic any prop.
 external pred names % generates the list of eigenvariable
   o:list any. % list of eigenvariables in order of age (young first)
   
-external pred occurs % checks if the constant occurs in the term
-  i:any, % a constant (global or eigenvariable)
+external pred occurs % checks if the atom occurs in the term
+  i:any, % an atom, that is a global constant or a bound name (aka eigenvariable)
   i:any. % a term
   
 % [closed_term T] unify T with a variable that has no eigenvariables in
diff --git a/tests/test_API.v b/tests/test_API.v
index 978d7fb50..38621e1fd 100644
--- a/tests/test_API.v
+++ b/tests/test_API.v
@@ -84,7 +84,7 @@ Elpi Query lp:{{
 
 Class foo (n : nat).
 Definition bar n {f : foo n} := n = n.
-Instance xxx : foo 3. Defined.
+#[local] Instance xxx : foo 3. Defined.
 
 Elpi Query lp:{{
 
@@ -623,7 +623,7 @@ Elpi Query lp:{{ coq.TC.declare-class {{:gref C }} }}.
 
 Axiom c : C nat.
 
-Instance foox : C nat := c.
+#[local] Instance foox : C nat := c.
 
 (****** CS **********************************)
 
diff --git a/tests/test_API2.v b/tests/test_API2.v
index b22859cf7..350687046 100644
--- a/tests/test_API2.v
+++ b/tests/test_API2.v
@@ -129,9 +129,9 @@ Elpi Query lp:{{
 
 (* Hints transparent *)
 
-Hint Opaque plus : core.
+#[local] Hint Opaque plus : core.
 Definition times := plus.
-Hint Transparent times : core.
+#[local] Hint Transparent times : core.
 
 Elpi Query lp:{{
 
@@ -156,7 +156,7 @@ Elpi Query lp:{{
 
 }}.
 
-Hint Opaque x : core.
+#[local] Hint Opaque x : core.
 
 Elpi Query lp:{{
   std.do! [
@@ -186,7 +186,7 @@ Elpi Query lp:{{
 
 }}.
 
-Hint Opaque x : core.
+#[local] Hint Opaque x : core.
 
 Elpi Query lp:{{
   std.do! [