Relying on the abstract notion of streams with location for parsing.

We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).

1 files changed, 7 insertions, 7 deletions

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index cb430efb40..9dec55e020 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -59,28 +59,28 @@ open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
-  Pcoq.Entry.of_parser "lpar_id_colon"
-    (fun _ strm ->
+  Pcoq.Entry.(of_parser "lpar_id_colon"
+    { parser_fun = fun strm ->
       let rec skip_to_rpar p n =
-        match List.last (Stream.npeek n strm) with
+        match List.last (LStream.npeek n strm) with
         | KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
         | KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1)
         | KEYWORD "." -> err ()
         | _ -> skip_to_rpar p (n+1) in
       let rec skip_names n =
-        match List.last (Stream.npeek n strm) with
+        match List.last (LStream.npeek n strm) with
         | IDENT _ | KEYWORD "_" -> skip_names (n+1)
         | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *)
         | _ -> err () in
       let rec skip_binders n =
-        match List.last (Stream.npeek n strm) with
+        match List.last (LStream.npeek n strm) with
         | KEYWORD "(" -> skip_binders (skip_names (n+1))
         | IDENT _ | KEYWORD "_" -> skip_binders (n+1)
         | KEYWORD ":=" -> ()
         | _ -> err () in
-      match stream_nth 0 strm with
+      match LStream.peek_nth 0 strm with
       | KEYWORD "(" -> skip_binders 2
-      | _ -> err ())
+      | _ -> err () })
 
 let lookup_at_as_comma =
   let open Pcoq.Lookahead in