If a custom entry has global, an argument-free abbreviation is valid …

…in this entry.

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

Note: More delicate would be to recognize that some given entry
support applicative nodes hence abbreviations with arguments.

interp/constrextern.ml

@@ -621,6 +621,10 @@ let is_projection nargs r =
 
 let is_hole = function CHole _ | CEvar _ -> true | _ -> false
 
+let isCRef_no_univ = function
+  | CRef (_,None) -> true
+  | _ -> false
+
 let is_significant_implicit a =
   not (is_hole (a.CAst.v))
 
@@ -1287,9 +1291,6 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
                   let args = extern_args (extern true) vars args in
                   CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args)
           | SynDefRule kn ->
-             match availability_of_entry_coercion custom InConstrEntrySomeLevel with
-             | None -> raise No_match
-             | Some coercion ->
               let l =
                 List.map (fun (c,(subentry,(scopt,scl))) ->
                   extern true (subentry,(scopt,scl@snd scopes)) vars c)
@@ -1299,7 +1300,10 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
               let args = fill_arg_scopes args argsscopes allscopes in
               let args = extern_args (extern true) vars args in
               let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in
-              insert_entry_coercion coercion c
+              if isCRef_no_univ c.CAst.v && entry_has_global custom then c
+             else match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+             | None -> raise No_match
+             | Some coercion -> insert_entry_coercion coercion c
       with
           No_match -> extern_notation allscopes vars t rules
 

test-suite/output/Notations4.out

@@ -14,6 +14,8 @@ Entry constr:myconstr is
      : nat
 [<< # 0 >>]
      : option nat
+[b + c]
+     : nat
 [1 {f 1}]
      : Expr
 fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
@@ -81,18 +83,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "stdin", line 219, characters 0-160:
+File "stdin", line 225, 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 232, characters 0-60:
+File "stdin", line 238, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 236, characters 0-64:
+File "stdin", line 242, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 241, characters 0-62:
+File "stdin", line 247, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing]
 3  %%  4
@@ -101,9 +103,9 @@ format. [notation-incompatible-format,parsing]
      : nat
 3   %%   4
      : nat
-File "stdin", line 269, characters 0-61:
+File "stdin", line 275, characters 0-61:
 Warning: The format modifier is irrelevant for only parsing rules.
 [irrelevant-format-only-parsing,parsing]
-File "stdin", line 273, characters 0-63:
+File "stdin", line 279, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]

test-suite/output/Notations4.v

@@ -22,6 +22,12 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a
 Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
 Check [ << # 0 >> ].
 
+(* Now check with global *)
+
+Axiom c : nat.
+Notation "x" := x (in custom myconstr at level 0, x global).
+Check [ b + c ].
+
 End A.
 
 Module B.