Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notations.

Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes

6 files changed, 49 insertions, 49 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 023705e169..5247c7b56a 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -309,9 +309,9 @@ Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
   : type_scope.
 
 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
-  (at level 200, x ident, p at level 200, right associativity) : type_scope.
+  (at level 200, x name, p at level 200, right associativity) : type_scope.
 Notation "'exists2' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q))
-  (at level 200, x ident, A at level 200, p at level 200, right associativity,
+  (at level 200, x name, A at level 200, p at level 200, right associativity,
     format "'[' 'exists2'  '/  ' x  :  A ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 
@@ -489,18 +489,18 @@ Module EqNotations.
     := (match H as p in (_ = y) return P with
         | eq_refl => H'
         end)
-         (at level 10, H' at level 10, y ident, p ident,
+         (at level 10, H' at level 10, y name, p name,
           format "'[' 'rew'  'dependent'  [ 'fun'  y  p  =>  P ]  '/    ' H  in  '/' H' ']'").
   Notation "'rew' 'dependent' -> [ 'fun' y p => P ] H 'in' H'"
     := (match H as p in (_ = y) return P with
         | eq_refl => H'
         end)
-         (at level 10, H' at level 10, y ident, p ident, only parsing).
+         (at level 10, H' at level 10, y name, p name, only parsing).
   Notation "'rew' 'dependent' <- [ 'fun' y p => P ] H 'in' H'"
     := (match eq_sym H as p in (_ = y) return P with
         | eq_refl => H'
         end)
-         (at level 10, H' at level 10, y ident, p ident,
+         (at level 10, H' at level 10, y name, p name,
           format "'[' 'rew'  'dependent'  <-  [ 'fun'  y  p  =>  P ]  '/    ' H  in  '/' H' ']'").
   Notation "'rew' 'dependent' [ P ] H 'in' H'"
     := (match H as p in (_ = y) return P y p with
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 84d40035bf..1a2c4ba171 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -96,19 +96,19 @@ Module Generic.
 (* begin hide *)
 (* Notations used in the proof. Hidden in coqdoc. *)
 
-Reserved Notation "'∀₁' x : A , B" (at level 200, x ident, A at level 200,right associativity).
+Reserved Notation "'∀₁' x : A , B" (at level 200, x name, A at level 200,right associativity).
 Reserved Notation "A '⟶₁' B" (at level 99, right associativity, B at level 200).
-Reserved Notation "'λ₁' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "'λ₁' x , u" (at level 200, x name, right associativity).
 Reserved Notation "f '·₁' x" (at level 5, left associativity).
-Reserved Notation "'∀₂' A , F" (at level 200, A ident, right associativity).
-Reserved Notation "'λ₂' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "'∀₂' A , F" (at level 200, A name, right associativity).
+Reserved Notation "'λ₂' x , u" (at level 200, x name, right associativity).
 Reserved Notation "f '·₁' [ A ]" (at level 5, left associativity).
-Reserved Notation "'∀₀' x : A , B" (at level 200, x ident, A at level 200,right associativity).
+Reserved Notation "'∀₀' x : A , B" (at level 200, x name, A at level 200,right associativity).
 Reserved Notation "A '⟶₀' B" (at level 99, right associativity, B at level 200).
-Reserved Notation "'λ₀' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "'λ₀' x , u" (at level 200, x name, right associativity).
 Reserved Notation "f '·₀' x" (at level 5, left associativity).
-Reserved Notation "'∀₀¹' A : U , F" (at level 200, A ident, right associativity).
-Reserved Notation "'λ₀¹' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "'∀₀¹' A : U , F" (at level 200, A name, right associativity).
+Reserved Notation "'λ₀¹' x , u" (at level 200, x name, right associativity).
 Reserved Notation "f '·₀' [ A ]" (at level 5, left associativity).
 
 (* end hide *)
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 9c8508bf39..b2bdd8099a 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -18,7 +18,7 @@ Set Implicit Arguments.
 
 Notation "{ ( x , y )  :  A  |  P }" :=
   (sig (fun anonymous : A => let (x,y) := anonymous in P))
-  (x ident, y ident, at level 10) : type_scope.
+  (x name, y name, at level 10) : type_scope.
 
 Declare Scope program_scope.
 Delimit Scope program_scope with prg.
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index d1cefeb552..a563dcbf95 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -335,19 +335,19 @@ Reserved Notation "[ 'predType' 'of' T ]" (at level 0,
 
 Reserved Notation "[ 'pred' : T | E ]" (at level 0,
   format "'[hv' [ 'pred' :  T  | '/ '  E ] ']'").
-Reserved Notation "[ 'pred' x | E ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x | E ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  | '/ '  E ] ']'").
-Reserved Notation "[ 'pred' x : T | E ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x : T | E ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  :  T  | '/ '  E ] ']'").
-Reserved Notation "[ 'pred' x | E1 & E2 ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x | E1 & E2 ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  | '/ '  E1  & '/ '  E2 ] ']'").
-Reserved Notation "[ 'pred' x : T | E1 & E2 ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x : T | E1 & E2 ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  :  T  | '/ '  E1  &  E2 ] ']'").
-Reserved Notation "[ 'pred' x 'in' A ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x 'in' A ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  'in'  A ] ']'").
-Reserved Notation "[ 'pred' x 'in' A | E ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x 'in' A | E ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  'in'  A  | '/ '  E ] ']'").
-Reserved Notation "[ 'pred' x 'in' A | E1 & E2 ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x 'in' A | E1 & E2 ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  'in'  A  | '/ '  E1  & '/ '  E2 ] ']'").
 
 Reserved Notation "[ 'qualify' x | P ]" (at level 0, x at level 99,
@@ -363,17 +363,17 @@ Reserved Notation "[ 'qualify' 'an' x | P ]" (at level 0, x at level 99,
 Reserved Notation "[ 'qualify' 'an' x : T | P ]" (at level 0, x at level 99,
   format "'[hv' [ 'qualify'  'an'  x  :  T  | '/ '  P ] ']'").
 
-Reserved Notation "[ 'rel' x y | E ]"  (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y | E ]"  (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  | '/ '  E ] ']'").
-Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  :  T  | '/ '  E ] ']'").
-Reserved Notation "[ 'rel' x y 'in' A & B | E ]" (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y 'in' A & B | E ]" (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  'in'  A  &  B  | '/ '  E ] ']'").
-Reserved Notation "[ 'rel' x y 'in' A & B ]" (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y 'in' A & B ]" (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  'in'  A  &  B ] ']'").
-Reserved Notation "[ 'rel' x y 'in' A | E ]" (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y 'in' A | E ]" (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  'in'  A  | '/ '  E ] ']'").
-Reserved Notation "[ 'rel' x y 'in' A ]" (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y 'in' A ]" (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  'in'  A ] ']'").
 
 Reserved Notation "[ 'mem' A ]" (at level 0, format "[ 'mem'  A ]").
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
index d0508bef2e..dc81b5cca7 100644
--- a/theories/ssr/ssreflect.v
+++ b/theories/ssr/ssreflect.v
@@ -110,7 +110,7 @@ Reserved Notation "'if' c 'then' vT 'else' vF" (at level 200,
 Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 200,
   c, R, vT, vF at level 200).
 Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 200,
-  c, R, vT, vF at level 200, x ident).
+  c, R, vT, vF at level 200, x name).
 
 Reserved Notation "x : T" (at level 100, right associativity,
   format "'[hv' x '/ '  :  T ']'").
diff --git a/theories/ssr/ssrfun.v b/theories/ssr/ssrfun.v
index e1442e1da2..ba66e04e4a 100644
--- a/theories/ssr/ssrfun.v
+++ b/theories/ssr/ssrfun.v
@@ -236,19 +236,19 @@ Reserved Notation "'fun' => E" (at level 200, format "'fun' =>  E").
 Reserved Notation "[ 'fun' : T => E ]" (at level 0,
   format "'[hv' [ 'fun' :  T  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' x => E ]" (at level 0,
-  x ident, format "'[hv' [ 'fun'  x  => '/ '  E ] ']'").
+  x name, format "'[hv' [ 'fun'  x  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' x : T => E ]" (at level 0,
-  x ident, format "'[hv' [ 'fun'  x  :  T  => '/ '  E ] ']'").
+  x name, format "'[hv' [ 'fun'  x  :  T  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' x y => E ]" (at level 0,
-  x ident, y ident, format "'[hv' [ 'fun'  x  y  => '/ '  E ] ']'").
+  x name, y name, format "'[hv' [ 'fun'  x  y  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' x y : T => E ]" (at level 0,
-  x ident, y ident, format "'[hv' [ 'fun'  x  y  :  T  => '/ '  E ] ']'").
+  x name, y name, format "'[hv' [ 'fun'  x  y  :  T  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' ( x : T ) y => E ]" (at level 0,
-  x ident, y ident, format "'[hv' [ 'fun'  ( x  :  T )  y  => '/ '  E ] ']'").
+  x name, y name, format "'[hv' [ 'fun'  ( x  :  T )  y  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' x ( y : T ) => E ]" (at level 0,
-  x ident, y ident, format "'[hv' [ 'fun'  x  ( y  :  T )  => '/ '  E ] ']'").
+  x name, y name, format "'[hv' [ 'fun'  x  ( y  :  T )  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" (at level 0,
-  x ident, y ident, format "[ 'fun'  ( x  :  T )  ( y  :  U )  =>  E ]" ).
+  x name, y name, format "[ 'fun'  ( x  :  T )  ( y  :  U )  =>  E ]" ).
 
 Reserved Notation "f =1 g" (at level 70, no associativity).
 Reserved Notation "f =1 g :> A" (at level 70, g at next level, A at level 90).
@@ -259,33 +259,33 @@ Reserved Notation "f \; g" (at level 60, right associativity,
   format "f  \; '/ '  g").
 
 Reserved Notation "{ 'morph' f : x / a >-> r }" (at level 0, f at level 99,
-  x ident, format "{ 'morph'  f  :  x  /  a  >->  r }").
+  x name, format "{ 'morph'  f  :  x  /  a  >->  r }").
 Reserved Notation "{ 'morph' f : x / a }" (at level 0, f at level 99,
-  x ident, format "{ 'morph'  f  :  x  /  a }").
+  x name, format "{ 'morph'  f  :  x  /  a }").
 Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'morph'  f  :  x  y  /  a  >->  r }").
+  x name, y name, format "{ 'morph'  f  :  x  y  /  a  >->  r }").
 Reserved Notation "{ 'morph' f : x y / a }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'morph'  f  :  x  y  /  a }").
+  x name, y name, format "{ 'morph'  f  :  x  y  /  a }").
 Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99,
-  x ident, format "{ 'homo'  f  :  x  /  a  >->  r }").
+  x name, format "{ 'homo'  f  :  x  /  a  >->  r }").
 Reserved Notation "{ 'homo' f : x / a }"  (at level 0, f at level 99,
-  x ident, format "{ 'homo'  f  :  x  /  a }").
+  x name, format "{ 'homo'  f  :  x  /  a }").
 Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'homo'  f  :  x  y  /  a  >->  r }").
+  x name, y name, format "{ 'homo'  f  :  x  y  /  a  >->  r }").
 Reserved Notation "{ 'homo' f : x y / a }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'homo'  f  :  x  y  /  a }").
+  x name, y name, format "{ 'homo'  f  :  x  y  /  a }").
 Reserved Notation "{ 'homo' f : x y /~ a }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'homo'  f  :  x  y  /~  a }").
+  x name, y name, format "{ 'homo'  f  :  x  y  /~  a }").
 Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99,
-  x ident, format "{ 'mono'  f  :  x  /  a  >->  r }").
+  x name, format "{ 'mono'  f  :  x  /  a  >->  r }").
 Reserved Notation "{ 'mono' f : x / a }" (at level 0, f at level 99,
-  x ident, format "{ 'mono'  f  :  x  /  a }").
+  x name, format "{ 'mono'  f  :  x  /  a }").
 Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'mono'  f  :  x  y  /  a  >->  r }").
+  x name, y name, format "{ 'mono'  f  :  x  y  /  a  >->  r }").
 Reserved Notation "{ 'mono' f : x y / a }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'mono'  f  :  x  y  /  a }").
+  x name, y name, format "{ 'mono'  f  :  x  y  /  a }").
 Reserved Notation "{ 'mono' f : x y /~ a }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'mono'  f  :  x  y  /~  a }").
+  x name, y name, format "{ 'mono'  f  :  x  y  /~  a }").
 
 Reserved Notation "@ 'id' T" (at level 10, T at level 8, format "@ 'id'  T").
 Reserved Notation "@ 'sval'" (at level 10, format "@ 'sval'").