doc: fix typo reference in doc of lazy discrimination tree (#6377)

This PR fix a bad reference in doc of lazy discrimination tree.
leanprover · Dec 13, 2024 · 58ffd15 · 58ffd15
1 parent bac34c7
commit 58ffd15
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean
@@ -15,7 +15,7 @@ population of imported modules for use in tactics.  It uses a lazy
 initialization strategy.
 
 The discrimination tree can be created through
-`createImportedEnvironment`. This creates a discrimination tree from all
+`createImportedDiscrTree`. This creates a discrimination tree from all
 imported modules in an environment using a callback that provides the
 entries as `InitEntry` values.