Moving bug numbers to BZ# format in the test-suite.

Compared to the original proposition (59a594b in #960), this commit
only changes files containing bug numbers that are also PR numbers.

29 files changed, 51 insertions, 52 deletions

diff --git a/test-suite/ideal-features/complexity/evars_subst.v b/test-suite/ideal-features/complexity/evars_subst.v
index b3dfb33cd..b9c359888 100644
--- a/test-suite/ideal-features/complexity/evars_subst.v
+++ b/test-suite/ideal-features/complexity/evars_subst.v
@@ -1,4 +1,4 @@
-(* Bug report #932 *)
+(* BZ#932 *)
 (* Expected time < 1.00s *)
 
 (* Let n be the number of let-in. The complexity comes from the fact
diff --git a/test-suite/ideal-features/evars_subst.v b/test-suite/ideal-features/evars_subst.v
index b3dfb33cd..b9c359888 100644
--- a/test-suite/ideal-features/evars_subst.v
+++ b/test-suite/ideal-features/evars_subst.v
@@ -1,4 +1,4 @@
-(* Bug report #932 *)
+(* BZ#932 *)
 (* Expected time < 1.00s *)
 
 (* Let n be the number of let-in. The complexity comes from the fact
diff --git a/test-suite/interactive/Back.v b/test-suite/interactive/Back.v
index b813a79ab..22364254d 100644
--- a/test-suite/interactive/Back.v
+++ b/test-suite/interactive/Back.v
@@ -1,5 +1,5 @@
 (* Check that reset remains synchronised with the compilation unit cache *)
-(* See bug #1030 *)
+(* See BZ#1030 *)
 
 Section multiset_defs.
   Require Import Plus.
diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v
index 220e2b369..0a6b1f06d 100644
--- a/test-suite/modules/objects2.v
+++ b/test-suite/modules/objects2.v
@@ -2,7 +2,7 @@
    the logical objects in the environment
 *)
 
-(* Bug #1118 (simplified version), submitted by Evelyne Contejean
+(* BZ#1118 (simplified version), submitted by Evelyne Contejean
   (used to failed in pre-V8.1 trunk because of a call to lookup_mind
    for structure objects)
 *)
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index fafb478ba..61ae4edbd 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -7,7 +7,7 @@ Check
              | a :: l => f a :: F _ _ f l
              end).
 
-(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf bug #860) *)
+(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf BZ#860) *)
 Check
   let fix f (m : nat) : nat :=
     match m with
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 7c9b89f9d..306532c0d 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -1,7 +1,7 @@
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(* Suggested by Pierre Casteran (bug #169) *)
+(* Suggested by Pierre Casteran (BZ#169) *)
 (* Argument 3 is needed to typecheck and should be printed *)
 Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x).
 Check (compose (C:=nat) S).
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 9a5edb813..75b66e463 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -7,12 +7,12 @@ Ltac f H := split; [a H|e H].
 Print Ltac f.
 
 (* Test printing of match context *)
-(* Used to fail after translator removal (see bug #1070) *)
+(* Used to fail after translator removal (see BZ#1070) *)
 
 Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
 Print Ltac g.
 
-(* Test an error message (#5390) *)
+(* Test an error message (BZ#5390) *)
 Lemma myid (P : Prop) : P <-> P.
 Proof. split; auto. Qed.
 
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index 69dc9aca7..d52a853aa 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -1,4 +1,4 @@
-(* Cf coqbugs #546 *)
+(* Cf BZ#546 *)
 
 Require Import Omega.
 
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 06f807f29..893d75b77 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -64,7 +64,7 @@ Check (fun x:I1 =>
   end).
 
 (* Check implicit parameters of inductive types (submitted by Pierre
-  Casteran and also implicit in #338) *)
+  Casteran and also implicit in BZ#338) *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -80,7 +80,7 @@ Inductive Finite (A : Set) : LList A -> Prop :=
   | Finite_LCons :
       forall (a : A) (l : LList A), Finite l -> Finite (LCons a l).
 
-(* Check positivity modulo reduction (cf bug #983) *)
+(* Check positivity modulo reduction (cf bug BZ#983) *)
 
 Record P:Type := {PA:Set; PB:Set}.
 
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 850f09434..45c71615f 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -1,6 +1,6 @@
 Axiom magic : False.
 
-(* Submitted by Dachuan Yu (bug #220) *)
+(* Submitted by Dachuan Yu (BZ#220) *)
 Fixpoint T (n : nat) : Type :=
   match n with
   | O => nat -> Prop
@@ -16,7 +16,7 @@ Lemma Inversion_RO : forall l : nat, R 0 Psi0 l -> Psi00 l.
 inversion 1.
 Abort.
 
-(* Submitted by Pierre Casteran (bug #540) *)
+(* Submitted by Pierre Casteran (BZ#540) *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -64,7 +64,7 @@ elim magic.
 elim magic.
 Qed.
 
-(* Submitted by Boris Yakobowski (bug #529) *)
+(* Submitted by Boris Yakobowski (BZ#529) *)
 (* Check that Inversion does not fail due to unnormalized evars *)
 
 Set Implicit Arguments.
@@ -100,7 +100,7 @@ intros a b H.
 inversion H.
 Abort.
 
-(* Check non-regression of bug #1968 *)
+(* Check non-regression of BZ#1968 *)
 
 Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t).
 Goal forall o, foo2 o -> 0 = 1.
@@ -130,7 +130,7 @@ Proof.
 intros. inversion H.
 Abort.
 
-(* Bug #2314 (simplified): check that errors do not show as anomalies *)
+(* BZ#2314 (simplified): check that errors do not show as anomalies *)
 
 Goal True -> True.
 intro.
@@ -158,7 +158,7 @@ reflexivity.
 Qed.
 
 (* Up to September 2014, Mapp below was called MApp0 because of a bug
-   in intro_replacing (short version of bug 2164.v)
+   in intro_replacing (short version of BZ#2164.v)
    (example taken from CoLoR) *)
 
 Parameter Term : Type.
diff --git a/test-suite/success/Mod_type.v b/test-suite/success/Mod_type.v
index d5e1a38cf..6c59bf6ed 100644
--- a/test-suite/success/Mod_type.v
+++ b/test-suite/success/Mod_type.v
@@ -1,4 +1,4 @@
-(* Check bug #1025 submitted by Pierre-Luc Carmel Biron *)
+(* Check BZ#1025 submitted by Pierre-Luc Carmel Biron *)
 
 Module Type FOO.
   Parameter A : Type.
@@ -18,7 +18,7 @@ Module Bar : BAR.
 
 End Bar.
 
-(* Check bug #2809: correct printing of modules with notations *)
+(* Check BZ#2809: correct printing of modules with notations *)
 
 Module C.
   Inductive test : Type :=
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 4d04f2cf9..e3f90f6d9 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -1,5 +1,5 @@
 (* Check that "where" clause behaves as if given independently of the  *)
-(* definition (variant of bug #1132 submitted by Assia Mahboubi) *)
+(* definition (variant of BZ#1132 submitted by Assia Mahboubi) *)
 
 Fixpoint plus1 (n m:nat) {struct n} : nat :=
    match n with
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index ecbf04e41..470e4f058 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -52,7 +52,7 @@ Lemma lem5 : (H > 0)%Z.
 Qed.
 End B.
 
-(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *)
+(* From Nicolas Oury (BZ#180): handling -> on Set (fixed Oct 2002) *)
 Lemma lem6 :
  forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z.
 intros.
@@ -86,7 +86,7 @@ intros;  omega.
 Qed.
 
 (* Check that the interpretation of mult on nat enforces its positivity *)
-(* Submitted by Hubert Thierry (bug #743) *)
+(* Submitted by Hubert Thierry (BZ#743) *)
 (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
 Lemma lem10 : forall n m:nat, le n (plus n (mult n m)).
 Proof.
diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v
index b8f8660e9..6fd936935 100644
--- a/test-suite/success/Omega0.v
+++ b/test-suite/success/Omega0.v
@@ -132,7 +132,7 @@ intros.
 omega.
 Qed.
 
-(* Magaud #240 *)
+(* Magaud BZ#240 *)
 
 Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
 intros.
diff --git a/test-suite/success/Omega2.v b/test-suite/success/Omega2.v
index c4d086a34..4e726335c 100644
--- a/test-suite/success/Omega2.v
+++ b/test-suite/success/Omega2.v
@@ -1,6 +1,6 @@
 Require Import ZArith Omega.
 
-(* Submitted by Yegor Bryukhov (#922) *)
+(* Submitted by Yegor Bryukhov (BZ#922) *)
 
 Open Scope Z_scope.
 
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
index 801ece9e3..0df3d5685 100644
--- a/test-suite/success/ROmega.v
+++ b/test-suite/success/ROmega.v
@@ -52,7 +52,7 @@ Lemma lem5 : (H > 0)%Z.
 Qed.
 End B.
 
-(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *)
+(* From Nicolas Oury (BZ#180): handling -> on Set (fixed Oct 2002) *)
 Lemma lem6 :
  forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z.
 intros.
@@ -88,7 +88,7 @@ romega with nat.
 Qed.
 
 (* Check that the interpretation of mult on nat enforces its positivity *)
-(* Submitted by Hubert Thierry (bug #743) *)
+(* Submitted by Hubert Thierry (BZ#743) *)
 (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
 Lemma lem10 : forall n m : nat, le n (plus n (mult n m)).
 Proof.
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
index 42730f2e1..3ddf6a40f 100644
--- a/test-suite/success/ROmega0.v
+++ b/test-suite/success/ROmega0.v
@@ -132,7 +132,7 @@ intros.
 romega.
 Qed.
 
-(* Magaud #240 *)
+(* Magaud BZ#240 *)
 
 Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
 Proof.
@@ -146,7 +146,7 @@ intros x y.
 romega.
 Qed.
 
-(* Besson #1298 *)
+(* Besson BZ#1298 *)
 
 Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False.
 Proof.
diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v
index 87e8c8e33..43eda67ea 100644
--- a/test-suite/success/ROmega2.v
+++ b/test-suite/success/ROmega2.v
@@ -1,6 +1,6 @@
 Require Import ZArith ROmega.
 
-(* Submitted by Yegor Bryukhov (#922) *)
+(* Submitted by Yegor Bryukhov (BZ#922) *)
 
 Open Scope Z_scope.
 
diff --git a/test-suite/success/Rename.v b/test-suite/success/Rename.v
index 0576f3c68..2789c6c9a 100644
--- a/test-suite/success/Rename.v
+++ b/test-suite/success/Rename.v
@@ -4,7 +4,7 @@ rename n into p.
 induction p; auto.
 Qed.
 
-(* Submitted by Iris Loeb (#842) *)
+(* Submitted by Iris Loeb (BZ#842) *)
 
 Section rename.
 
diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v
index 361c787e2..76aac39a5 100644
--- a/test-suite/success/Try.v
+++ b/test-suite/success/Try.v
@@ -1,5 +1,5 @@
 (* To shorten interactive scripts, it is better that Try catches
-   non-existent names in Unfold [cf bug #263] *)
+   non-existent names in Unfold [cf BZ#263] *)
 
 Lemma lem1 : True.
 try unfold i_dont_exist.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 90a60daa6..0219c3bfd 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -12,7 +12,7 @@ assumption.
 assumption.
 Qed.
 
-(* Simplification of bug 711 *)
+(* Simplification of BZ#711 *)
 
 Parameter f : true = false.
 Goal let p := f in True.
@@ -37,7 +37,7 @@ Goal True.
 case Refl || ecase Refl.
 Abort.
 
-(* Submitted by B. Baydemir (bug #1882) *)
+(* Submitted by B. Baydemir (BZ#1882) *)
 
 Require Import List.
 
@@ -385,7 +385,7 @@ intros.
 Fail destruct H.
 Abort.
 
-(* Check keep option (bug #3791) *)
+(* Check keep option (BZ#3791) *)
 
 Goal forall b:bool, True.
 intro b.
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index c36313ec1..627794832 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -23,7 +23,7 @@ Definition f1 frm0 a1 : B := f frm0 a1.
 (* Checks that solvable ? in the type part of the definition are harmless *)
 Definition f2 frm0 a1 : B := f frm0 a1.
 
-(* Checks that sorts that are evars are handled correctly (bug 705) *)
+(* Checks that sorts that are evars are handled correctly (BZ#705) *)
 Require Import List.
 
 Fixpoint build (nl : list nat) :
@@ -58,7 +58,7 @@ Check
     (forall y n : nat, {q : nat | y = q * n}) ->
     forall n : nat, {q : nat | x = q * n}).
 
-(* Check instantiation of nested evars (bug #1089) *)
+(* Check instantiation of nested evars (BZ#1089) *)
 
 Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))).
 
@@ -188,7 +188,7 @@ Abort.
 
 End Additions_while.
 
-(* Two examples from G. Melquiond (bugs #1878 and #1884) *)
+(* Two examples from G. Melquiond (BZ#1878 and BZ#1884) *)
 
 Parameter F1 G1 : nat -> Prop.
 Goal forall x : nat, F1 x -> G1 x.
@@ -207,7 +207,7 @@ Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) :=
   | (existT _ k v)::l' => (existT _ k v):: (filter A l')
   end.
 
-(* Bug #2000: used to raise Out of memory in 8.2 while it should fail by
+(* BZ#2000: used to raise Out of memory in 8.2 while it should fail by
    lack of information on the conclusion of the type of j *)
 
 Goal True.
@@ -381,7 +381,7 @@ Section evar_evar_occur.
   Check match g _ with conj a b => f _ a b end.
 End evar_evar_occur.
 
-(* Eta expansion (bug #2936) *)
+(* Eta expansion (BZ#2936) *)
 Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }.
 Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri {
   tri0 : forall a b c, R a b -> S a c -> T b c
diff --git a/test-suite/success/if.v b/test-suite/success/if.v
index 9fde95e80..c81d2b9bf 100644
--- a/test-suite/success/if.v
+++ b/test-suite/success/if.v
@@ -3,7 +3,7 @@
 
 Check (fun b : bool => if b then Type else nat).
 
-(* Check correct use of if-then-else predicate annotation (cf bug 690) *)
+(* Check correct use of if-then-else predicate annotation (cf BZ#690) *)
 
 Check fun b : bool =>
  if b as b0 return (if b0 then b0 = true else b0 = false)
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index ee69df977..a329894aa 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -1,5 +1,5 @@
 (* Thinning introduction hypothesis must be done after all introductions *)
-(* Submitted by Guillaume Melquiond (bug #1000) *)
+(* Submitted by Guillaume Melquiond (BZ#1000) *)
 
 Goal forall A, A -> True.
 intros _ _.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 29e373eaa..0f22a1f0a 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -147,7 +147,7 @@ check_binding ipattern:(H).
 Abort.
 
 (* Check that variables explicitly parsed as ltac variables are not
-   seen as intro pattern or constr (bug #984) *)
+   seen as intro pattern or constr (BZ#984) *)
 
 Ltac afi tac := intros; tac.
 Goal 1 = 2.
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 352abb2af..b8a8ff756 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -31,7 +31,7 @@ Proof.
   end).
 Abort.
 
-(* Submitted by Roland Zumkeller (bug #888) *)
+(* Submitted by Roland Zumkeller (BZ#888) *)
 
 (* The Fix and CoFix rules expect a subgoal even for closed components of the
    (co-)fixpoint *)
@@ -43,7 +43,7 @@ Goal nat -> nat.
 exact 0.
 Qed.
 
-(* Submitted by Roland Zumkeller (bug #889) *)
+(* Submitted by Roland Zumkeller (BZ#889) *)
 
 (* The types of metas were in metamap and they were not updated when
    passing through a binder *)
@@ -56,7 +56,7 @@ Goal forall n : nat, nat -> n = 0.
                                       end).
 Abort.
 
-(* Submitted by Roland Zumkeller (bug #931) *)
+(* Submitted by Roland Zumkeller (BZ#931) *)
 (* Don't turn dependent evar into metas *)
 
 Goal (forall n : nat, n = 0 -> Prop) -> Prop.
@@ -65,7 +65,7 @@ intro P.
 reflexivity.
 Abort.
 
-(* Submitted by Jacek Chrzaszcz (bug #1102) *)
+(* Submitted by Jacek Chrzaszcz (BZ#1102) *)
 
 (* le problème a été résolu ici par normalisation des evars présentes
    dans les types d'evars, mais le problème reste a priori ouvert dans
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index 5b87e877b..1bfb8580b 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -1,6 +1,6 @@
 Require Import TestSuite.admit.
 (* Check that inversion of names of mutual inductive fixpoints works *)
-(* (cf bug #1031) *)
+(* (cf BZ#1031) *)
 
 Inductive tree : Set :=
 | node : nat -> forest -> tree
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 6f7498d65..1ffc02673 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -43,7 +43,7 @@ Check (fun _h1 => (zenon_notall nat _ (fun _T_0 =>
           (fun _h2 => (zenon_noteq _ _T_0 _h2))) _h1)).
 
 
-(* Core of an example submitted by Ralph Matthes (#849)
+(* Core of an example submitted by Ralph Matthes (BZ#849)
 
    It used to fail because of the K-variable x in the type of "sum_rec ..."
    which was not in the scope of the evar ?B. Solved by a head
@@ -131,7 +131,7 @@ try case nonemptyT_intro. (* check that it fails w/o anomaly *)
 Abort.
 
 (* Test handling of return type and when it is decided to make the
-   predicate dependent or not - see "bug" #1851 *)
+   predicate dependent or not - see "bug" BZ#1851 *)
 
 Goal forall X (a:X) (f':nat -> X), (exists f : nat -> X, True).
 intros.
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index fc74225d7..286340459 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -20,8 +20,7 @@ intro P; pattern P.
 apply lem2.
 Abort.
 
-(* Check managing of universe constraints in inversion *)
-(* Bug report #855 *)
+(* Check managing of universe constraints in inversion (BZ#855) *)
 
 Inductive dep_eq : forall X : Type, X -> X -> Prop :=
   | intro_eq : forall (X : Type) (f : X), dep_eq X f f
@@ -40,7 +39,7 @@ Proof.
 Abort.
 
 
-(* Submitted by Bas Spitters (bug report #935) *)
+(* Submitted by Bas Spitters (BZ#935) *)
 
 (* This is a problem with the status of the type in LetIn: is it a
    user-provided one or an inferred one? At the current time, the