aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/extend.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/extend.mli')
-rw-r--r--parsing/extend.mli5
1 files changed, 0 insertions, 5 deletions
diff --git a/parsing/extend.mli b/parsing/extend.mli
index c9558a970..80a0e4448 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -113,11 +113,6 @@ type 'pat unparsing_hunk =
| UNP_FNL
| UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk
-(*val subst_unparsing_hunk :
- substitution -> (substitution -> 'pat -> 'pat) ->
- 'pat unparsing_hunk -> 'pat unparsing_hunk
-*)
-
(* Checks if the precedence of the parent printer (None means the
highest precedence), and the child's one, follow the given
relation. *)