Fix scope of notations

Author: gares

HB/lock.elpi

@@ -14,7 +14,7 @@ lock-def Name AritySkel BoSkel :- std.do! [
   private.lock-module-type NameTy Ty Bo Signature,
   private.lock-module-body Signature Name Ty Bo C,
 
-  log.coq.notation.add-abbreviation Name 0 (global (const C)) ff _,
+  @global! => log.coq.notation.add-abbreviation Name 0 (global (const C)) ff _,
 ].
 
 namespace private {

tests/lock.v

@@ -8,8 +8,14 @@ HB.lock Definition bar : nat1 := 3.
 
 HB.lock Definition baz n : nat := 3 + n.
 
+Module Import X.
+
 Axiom bigbody : Type -> Type -> Type.
 Axiom bigop : forall R I : Type, R -> list I -> (I -> bigbody R I) -> R.
 
-HB.lock Definition xxx := bigop.
+HB.lock Definition big := bigop.
+
+End X.
+
+About big.