Merge PR #960: Uniformize references to Bugzilla

34 files changed, 69 insertions, 73 deletions

diff --git a/CHANGES b/CHANGES
index f59bd5141c..640ab4aa50 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,10 +15,7 @@ Tactics
   profiling, and "Set NativeCompute Profile Filename" customizes
   the profile filename.
 - The tactic "omega" is now aware of the bodies of context variables
-  such as "x := 5 : Z" (see bug #148). This could be disabled via
-  Unset Omega UseLocalDefs.
-- The tactic "omega" is now aware of the bodies of context variables
-  such as "x := 5 : Z" (see bug #148). This could be disabled via
+  such as "x := 5 : Z" (see BZ#148). This could be disabled via
   Unset Omega UseLocalDefs.
 - The tactic "romega" is also aware now of the bodies of context variables.
 
@@ -2397,7 +2394,7 @@ Tactics
   a registered setoid equality before starting to reduce in H. This is unlikely
   to break any script. Should this happen nonetheless, one can insert manually
   some "unfold ... in H" before rewriting.
-- Fixed various bugs about (setoid) rewrite ... in ... (in particular #1101)
+- Fixed various bugs about (setoid) rewrite ... in ... (in particular BZ#1101)
 - "rewrite ... in" now accepts a clause as place where to rewrite instead of
   juste a simple hypothesis name. For instance:
    rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H
@@ -2974,11 +2971,11 @@ Incompatibilities
 Bugs
 
 - Improved localisation of errors in Syntactic Definitions
-- Induction principle creation failure in presence of let-in fixed (#238)
-- Inversion bugs fixed (#212 and #220)
-- Omega bug related to Set fixed (#180)
-- Type-checking inefficiency of nested destructuring let-in fixed (#216)
-- Improved handling of let-in during holes resolution phase (#239)
+- Induction principle creation failure in presence of let-in fixed (BZ#238)
+- Inversion bugs fixed (BZ#212 and BZ#220)
+- Omega bug related to Set fixed (BZ#180)
+- Type-checking inefficiency of nested destructuring let-in fixed (BZ#216)
+- Improved handling of let-in during holes resolution phase (BZ#239)
 
 Efficiency
 
@@ -2991,18 +2988,18 @@ Changes from V7.3 to V7.3.1
 Bug fixes
 
   - Corrupted Field tactic and Match Context tactic construction fixed
-  - Checking of names already existing in Assert added (PR#182)
-  - Invalid argument bug in Exact tactic solved (PR#183)
-  - Colliding bound names bug fixed (PR#202)
-  - Wrong non-recursivity test for Record fixed (PR#189)
-  - Out of memory/seg fault bug related to parametric inductive fixed (PR#195)
+  - Checking of names already existing in Assert added (BZ#182)
+  - Invalid argument bug in Exact tactic solved (BZ#183)
+  - Colliding bound names bug fixed (BZ#202)
+  - Wrong non-recursivity test for Record fixed (BZ#189)
+  - Out of memory/seg fault bug related to parametric inductive fixed (BZ#195)
   - Setoid_replace/Setoid_rewrite bug wrt "==" fixed
 
 Misc
 
   - Ocaml version >= 3.06 is needed to compile Coq from sources
   - Simplification of fresh names creation strategy for Assert, Pose and
-    LetTac (PR#192)
+    LetTac (BZ#192)
 
 Changes from V7.2 to V7.3
 =========================
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index cf97ae3ab8..4bc3dba36e 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -54,7 +54,7 @@ but also a few steps toward a more user-friendly extraction:
 
 * bug fixes: 
 - many concerning Records. 
-- a Stack Overflow with mutual inductive (PR#320)
+- a Stack Overflow with mutual inductive (BZ#320)
 - some optimizations have been removed since they were not type-safe:
   For example if e has type:  type 'x a = A
   Then:       match e with A -> A     -----X---->    e
@@ -125,7 +125,7 @@ but also a few steps toward a more user-friendly extraction:
 
   - the dummy constant "__" have changed. see README
 
-  - a few bug-fixes (#191 and others)
+  - a few bug-fixes (BZ#191 and others)
 
 7.2 -> 7.3
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 0f537abece..f708307c38 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -145,7 +145,7 @@ let rec pp_expr par env args =
     | MLrel n ->
 	let id = get_db_name n env in
         (* Try to survive to the occurrence of a Dummy rel.
-           TODO: we should get rid of this hack (cf. #592) *)
+           TODO: we should get rid of this hack (cf. BZ#592) *)
         let id = if Id.equal id dummy_name then Id.of_string "__" else id in
         apply (Id.print id)
     | MLapp (f,args') ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6f7e61f6ba..e8a78d72d6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2471,7 +2471,7 @@ let exceed_bound n = function
 
   (* We delay thinning until the completion of the whole intros tactic
      to ensure that dependent hypotheses are cleared in the right
-     dependency order (see bug #1000); we use fresh names, not used in
+     dependency order (see BZ#1000); we use fresh names, not used in
      the tactic, for the hyps to clear *)
   (* In [intro_patterns_core b avoid ids thin destopt bound n tac patl]:
      [b]: compatibility flag, if false at toplevel, do not complete incomplete
diff --git a/test-suite/ideal-features/complexity/evars_subst.v b/test-suite/ideal-features/complexity/evars_subst.v
index b3dfb33cdc..b9c3598887 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 b3dfb33cdc..b9c3598887 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 b813a79ab2..22364254dc 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 220e2b3694..0a6b1f06de 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 fafb478bad..61ae4edbd1 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 7c9b89f9d2..306532c0df 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 9a5edb813d..75b66e463a 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 69dc9aca78..d52a853aae 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 06f807f29a..893d75b77f 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 850f094348..45c71615fc 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 d5e1a38cf5..6c59bf6edb 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 4d04f2cf9b..e3f90f6d94 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 ecbf04e412..470e4f0580 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 b8f8660e9c..6fd936935c 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 c4d086a348..4e726335c9 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 801ece9e3d..0df3d5685d 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 42730f2e16..3ddf6a40fb 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 87e8c8e33e..43eda67ea3 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 0576f3c68f..2789c6c9a6 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 361c787e25..76aac39a55 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 90a60daa66..0219c3bfdf 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 c36313ec16..627794832d 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 9fde95e80d..c81d2b9bf1 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 ee69df9774..a329894aad 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 29e373eaa5..0f22a1f0a0 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 352abb2af5..b8a8ff7561 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 5b87e877bf..1bfb8580b3 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 6f7498d659..1ffc026730 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 fc74225d76..2863404590 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
diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v
index 886533586f..87b7a9a3be 100644
--- a/theories/Init/Tauto.v
+++ b/theories/Init/Tauto.v
@@ -27,7 +27,7 @@ Local Ltac simplif flags :=
       | id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id
       | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ =>
     (* generalize (id0 id1); intro; clear id0 does not work
-       (see Marco Maggiesi's bug PR#301)
+       (see Marco Maggiesi's BZ#301)
     so we instead use Assert and exact. *)
     assert X2; [exact (id0 id1) | clear id0]
       | id: forall (_ : ?X1), ?X2|- _ =>