From 97aac6a7cf1bab3226f979b55e37d61f22c2f358 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Dec 2019 11:35:14 +0100
Subject: Renaming confusingly-named insert_coercion into
 insert_entry_coercion.

This is to avoid confusion with typing coercions.

No change of semantics.
---
 interp/constrextern.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7a14ca3e48..0c29806774 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -282,9 +282,9 @@ let insert_pat_alias ?loc p = function
   | Anonymous -> p
   | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na))
 
-let rec insert_coercion ?loc l c = match l with
+let rec insert_entry_coercion ?loc l c = match l with
   | [] -> c
-  | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_coercion ?loc l c],[],[],[]))
+  | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_entry_coercion ?loc l c],[],[],[]))
 
 let rec insert_pat_coercion ?loc l c = match l with
   | [] -> c
@@ -849,7 +849,7 @@ let extern_possible_prim_token (custom,scopes) r =
    | Some coercion ->
    match availability_of_prim_token n sc scopes with
    | None -> raise No_match
-   | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+   | Some key -> insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
 
 let filter_enough_applied nargs l =
   match nargs with
@@ -1081,7 +1081,7 @@ let rec extern inctx ?impargs scopes vars r =
 
   | GFloat f -> extern_float f (snd scopes)
 
-  in insert_coercion coercion (CAst.make ?loc c)
+  in insert_entry_coercion coercion (CAst.make ?loc c)
 
 and extern_typ ?impargs (subentry,(_,scopes)) =
   extern true ?impargs (subentry,(Notation.current_type_scope_name (),scopes))
@@ -1279,7 +1279,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
                       pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
                       binderlists in
                   let c = make_notation loc specific_ntn (l,ll,bl,bll) in
-                  let c = insert_coercion coercion (insert_delimiters c key) in
+                  let c = insert_entry_coercion coercion (insert_delimiters c key) in
                   let args = fill_arg_scopes args argsscopes allscopes in
                   let args = extern_args (extern true) vars args in
                   CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args)
@@ -1296,7 +1296,7 @@ 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_coercion coercion c
+              insert_entry_coercion coercion c
       with
           No_match -> extern_notation allscopes vars t rules
 
-- 
cgit v1.2.3


From 9aefd708109658a8a17412e1fd7cc95bff454050 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 30 Dec 2019 17:18:33 +0100
Subject: 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: It would be more delicate to recognize that some given entry
support applicative nodes hence abbreviations with arguments.
---
 interp/constrextern.ml           | 12 ++++++++----
 test-suite/output/Notations4.out | 14 ++++++++------
 test-suite/output/Notations4.v   |  6 ++++++
 3 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0c29806774..0396e556cf 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -615,6 +615,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))
 
@@ -1284,9 +1288,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)
@@ -1296,7 +1297,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
 
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index e121b5e86c..8948518b3b 100644
--- a/test-suite/output/Notations4.out
+++ b/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]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 1cf0d919b1..08a4480e8a 100644
--- a/test-suite/output/Notations4.v
+++ b/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.
-- 
cgit v1.2.3


From 33aaa5d64771c3644de4771338c371ce6b865647 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 Apr 2020 17:23:44 +0200
Subject: 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.
---
 interp/constrextern.ml           |  6 ++++--
 test-suite/output/Notations4.out | 14 ++++++++------
 test-suite/output/Notations4.v   |  1 +
 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.
 
-- 
cgit v1.2.3