From b8ae2de5be242bbd1e34ec974627c81f99b16d23 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Oct 2016 22:51:09 +0200
Subject: Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
 done by the Ppcmd_comment token) and so that lexing/parsing side-effects are
 collected at the same place, i.e. in CLexer.

---
 lib/pp.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index 3bd560812e..f607e99dba 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -23,8 +23,7 @@ val ws    : int -> std_ppcmds
 val mt    : unit -> std_ppcmds
 val ismt  : std_ppcmds -> bool
 
-val comment  : int -> std_ppcmds
-val comments : ((int * int) * string) list ref
+val comment  : string list -> std_ppcmds
 
 (** {6 Manipulation commands} *)
 
-- 
cgit v1.2.3