Adapting standard library, doc and test suite to ident->name renaming.

11 files changed, 58 insertions, 56 deletions

diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index f7ce7f1c6c..aa754ab63d 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -490,10 +490,10 @@ We need some infrastructure for that.
     Definition id {T} {t : T} (x : phantom t) := x.
 
     Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p)
-      (at level 50, v ident, only parsing).
+      (at level 50, v name, only parsing).
 
     Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p)
-      (at level 50, v ident, only parsing).
+      (at level 50, v name, only parsing).
 
     Notation "'Error : t : s" := (unify _ t (Some s))
       (at level 50, format "''Error' : t : s").
diff --git a/test-suite/bugs/closed/bug_9517.v b/test-suite/bugs/closed/bug_9517.v
index bb43edbe74..93ed94df39 100644
--- a/test-suite/bugs/closed/bug_9517.v
+++ b/test-suite/bugs/closed/bug_9517.v
@@ -2,6 +2,7 @@ Declare Custom Entry expr.
 Declare Custom Entry stmt.
 Notation "x" := x (in custom stmt, x ident).
 Notation "x" := x (in custom expr, x ident).
+Notation "'_'" := _ (in custom expr).
 
 Notation "1" := 1 (in custom expr).
 
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index bcb2468792..05712eaac7 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -62,7 +62,7 @@ Check `(∀ n p : A, n=p).
 
 Notation "'let'' f x .. y  :=  t 'in' u":=
   (let f := fun x => .. (fun y => t) .. in u)
-  (f ident, x closed binder, y closed binder, at level 200,
+  (f name, x closed binder, y closed binder, at level 200,
    right associativity).
 
 Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
@@ -93,7 +93,7 @@ End A.
 
 Notation "'mylet' f [ x ; .. ; y ]  :=  t 'in' u":=
   (let f := fun x => .. (fun y => t) .. in u)
-  (f ident, x closed binder, y closed binder, at level 200,
+  (f name, x closed binder, y closed binder, at level 200,
    right associativity).
 
 Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
@@ -104,7 +104,7 @@ Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
 (* Old request mentioned again on coq-club 20/1/2012 *)
 
 Notation "#  x : T => t" := (fun x : T => t)
-  (at level 0, t at level 200, x ident).
+  (at level 0, t at level 200, x name).
 
 Check # x : nat => x.
 Check # _ : nat => 2.
@@ -116,7 +116,7 @@ Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
 
 (* Check bug #4854 *)
-Notation "% i" := (fun i : nat => i) (at level 0, i ident).
+Notation "% i" := (fun i : nat => i) (at level 0, i name).
 Check %i.
 Check %j.
 
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 04a91c14d9..6c714fc624 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -305,7 +305,7 @@ Module E.
 Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop :=
   myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q.
 Notation "'myexists2' x : A , p & q" := (myex2 (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 "'[' 'myexists2'  '/  ' x  :  A ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index ebc1426fc8..ce488fe18d 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -327,6 +327,7 @@ Module P.
 
   Module NotationMixedTermBinderAsIdent.
 
+  Set Warnings "-deprecated-ident-entry". (* We do want ident! *)
   Notation "▢_ n P" := (pseudo_force n (fun n => P))
     (at level 0, n ident, P at level 9, format "▢_ n  P").
   Check exists p, ▢_p (p >= 1).
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'").