If a custom entry has global, a bound variable is valid in this entry.

This is due to "global" being a syntactic notation, thus including ident.

Parsing was automatically supporting this. This commit adds support for printing.

3 files changed, 13 insertions, 8 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0396e556cf..a37bac3275 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -453,7 +453,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
     with No_match ->
     let loc = pat.CAst.loc in
     match DAst.get pat with
-    | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+    | PatVar (Name id) when entry_has_global custom || entry_has_ident custom ->
+      CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
     | pat ->
     match availability_of_entry_coercion custom InConstrEntrySomeLevel with
     | None -> raise No_match
@@ -935,7 +936,8 @@ let rec extern inctx ?impargs scopes vars r =
   match DAst.get r with
   | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us)
 
-  | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id)
+  | GVar id when entry_has_global (fst scopes) || entry_has_ident (fst scopes) ->
+      CAst.make ?loc (extern_var ?loc id)
 
   | c ->
 
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 8948518b3b..f48eaac4c9 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -16,6 +16,8 @@ Entry constr:myconstr is
      : option nat
 [b + c]
      : nat
+fun a : nat => [a + a]
+     : nat -> nat
 [1 {f 1}]
      : Expr
 fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
@@ -83,18 +85,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "stdin", line 225, characters 0-160:
+File "stdin", line 226, characters 0-160:
 Warning: Notation "∀ _ .. _ , _" was already defined with a different format
 in scope type_scope. [notation-incompatible-format,parsing]
 ∀x : nat,x = x
      : Prop
-File "stdin", line 238, characters 0-60:
+File "stdin", line 239, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 242, characters 0-64:
+File "stdin", line 243, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 247, characters 0-62:
+File "stdin", line 248, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing]
 3  %%  4
@@ -103,9 +105,9 @@ format. [notation-incompatible-format,parsing]
      : nat
 3   %%   4
      : nat
-File "stdin", line 275, characters 0-61:
+File "stdin", line 276, characters 0-61:
 Warning: The format modifier is irrelevant for only parsing rules.
 [irrelevant-format-only-parsing,parsing]
-File "stdin", line 279, characters 0-63:
+File "stdin", line 280, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 08a4480e8a..4d4b37a8b2 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -27,6 +27,7 @@ Check [ << # 0 >> ].
 Axiom c : nat.
 Notation "x" := x (in custom myconstr at level 0, x global).
 Check [ b + c ].
+Check fun a => [ a + a ].
 
 End A.