From d0252cac3167ef1e5cd26c1b9b40aea06d343413 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 17:48:57 +0200
Subject: More consistent writing of de Bruijn.

---
 tactics/dnet.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/dnet.mli b/tactics/dnet.mli
index 9f29c60b60..565a916f8e 100644
--- a/tactics/dnet.mli
+++ b/tactics/dnet.mli
@@ -26,7 +26,7 @@
    distincts, or you'll get unexpected behaviours.
 
    Warning 2: This structure is perfect, i.e. the set of candidates
-   returned is equal to the set of solutions. Beware of DeBruijn
+   returned is equal to the set of solutions. Beware of de Bruijn
    shifts and sorts subtyping though (which makes the comparison not
    symmetric, see term_dnet.ml).
 
-- 
cgit v1.2.3