fix warning

yoichi-at-bedrock · May 9, 2022 · 2a511a7 · 2a511a7
1 parent 7c07015
commit 2a511a7
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 8 deletions.
diff --git 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
@@ -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
@@ -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! [