aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/term_dnet.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli
index 2c748f9c9..7bce57789 100644
--- a/tactics/term_dnet.mli
+++ b/tactics/term_dnet.mli
@@ -26,7 +26,7 @@ open Mod_subst
The results returned here are perfect, since post-filtering is done
inside here.
- See lib/dnet.mli for more details.
+ See tactics/dnet.mli for more details.
*)
(** Identifiers to store (right hand side of the association) *)