From 56b562e057bbce736786cf1df16ba6e40dde8f30 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 19 Oct 2017 16:25:40 +0200
Subject: Moving bug numbers to BZ# format in the source code.

Compared to the original proposition (01f848d in #960), this commit
only changes files containing bug numbers that are also PR numbers.
---
 plugins/extraction/CHANGES    | 4 ++--
 plugins/extraction/haskell.ml | 2 +-
 tactics/tactics.ml            | 2 +-
 theories/Init/Tauto.v         | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

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/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|- _ =>
-- 
cgit v1.2.3