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.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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