Remove the unsafe camlp5 API from the Coq codebase.

7 files changed, 22 insertions, 24 deletions

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 7e707b423a..8f0440a2a4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -145,7 +145,6 @@ END
 
 {
 
-module Gram = Pcoq.Gram
 module Vernac = Pvernac.Vernac_
 module Tactic = Pltac
 
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index c4c4e51ecc..156ee94a66 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -332,7 +332,7 @@ END
 
 let local_test_lpar_id_colon =
   let err () = raise Stream.Failure in
-  Pcoq.Gram.Entry.of_parser "lpar_id_colon"
+  Pcoq.Entry.of_parser "lpar_id_colon"
     (fun strm ->
       match Util.stream_nth 0 strm with
         | Tok.KEYWORD "(" ->
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index bd8a097154..338839ee96 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -70,7 +70,7 @@ let _ =
 
 (* Hack to parse "[ id" without dropping [ *)
 let test_bracket_ident =
-  Gram.Entry.of_parser "test_bracket_ident"
+  Pcoq.Entry.of_parser "test_bracket_ident"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "[" ->
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index e29f78af5b..ef18dd6cdc 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -45,7 +45,6 @@ let with_tac f tac =
  * Subtac. These entries are named Subtac.<foo>
  *)
 
-module Gram = Pcoq.Gram
 module Tactic = Pltac
 
 open Pcoq
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 0ce0fbd0cd..46ea3819ac 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -39,7 +39,7 @@ let err () = raise Stream.Failure
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
 let test_lpar_id_coloneq =
-  Gram.Entry.of_parser "lpar_id_coloneq"
+  Pcoq.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -53,7 +53,7 @@ let test_lpar_id_coloneq =
 
 (* Hack to recognize "(x)" *)
 let test_lpar_id_rpar =
-  Gram.Entry.of_parser "lpar_id_coloneq"
+  Pcoq.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -67,7 +67,7 @@ let test_lpar_id_rpar =
 
 (* idem for (x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
-  Gram.Entry.of_parser "test_lpar_idnum_coloneq"
+  Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -84,7 +84,7 @@ open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
-  Gram.Entry.of_parser "lpar_id_colon"
+  Pcoq.Entry.of_parser "lpar_id_colon"
     (fun strm ->
       let rec skip_to_rpar p n =
 	match List.last (Stream.npeek n strm) with
@@ -108,7 +108,7 @@ let check_for_coloneq =
       | _ -> err ())
 
 let lookup_at_as_comma =
-  Gram.Entry.of_parser "lookup_at_as_comma"
+  Pcoq.Entry.of_parser "lookup_at_as_comma"
     (fun strm ->
       match stream_nth 0 strm with
 	| KEYWORD (","|"at"|"as") -> ()
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 7c91860228..2dff0cc84f 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -268,16 +268,16 @@ let negate_parser f x =
   | Some _ -> raise Stream.Failure 
 
 let test_not_ssrslashnum =
-  Pcoq.Gram.Entry.of_parser
+  Pcoq.Entry.of_parser
     "test_not_ssrslashnum" (negate_parser test_ssrslashnum10)
 let test_ssrslashnum00 =
-  Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
+  Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
 let test_ssrslashnum10 =
-  Pcoq.Gram.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
+  Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
 let test_ssrslashnum11 =
-  Pcoq.Gram.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
+  Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
 let test_ssrslashnum01 =
-  Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
+  Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
 
 }
 
@@ -470,7 +470,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "@" -> xWithAt
   | _ -> xNoFlag
 
-let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 (* New kinds of terms *)
 
@@ -481,7 +481,7 @@ let input_term_annotation strm =
   | Tok.KEYWORD "@" :: _ -> `At
   | _ -> `None
 let term_annotation =
-  Gram.Entry.of_parser "term_annotation" input_term_annotation
+  Pcoq.Entry.of_parser "term_annotation" input_term_annotation
 
 (* terms *)
 
@@ -800,7 +800,7 @@ let reject_ssrhid strm =
       | _ -> ())
   | _ -> ()
 
-let test_nohidden = Pcoq.Gram.Entry.of_parser "test_ssrhid" reject_ssrhid
+let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
 
 }
 
@@ -961,7 +961,7 @@ let accept_ssrfwdid strm =
   | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm
   | _ -> raise Stream.Failure
 
-let test_ssrfwdid = Gram.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid
+let test_ssrfwdid = Pcoq.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid
 
 }
 
@@ -1540,7 +1540,7 @@ let accept_ssrseqvar strm =
      accept_before_syms_or_ids ["["] ["first";"last"] strm
   | _ -> raise Stream.Failure
 
-let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
+let test_ssrseqvar = Pcoq.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
 
 let swaptacarg (loc, b) = (b, []), Some (TacId [])
 
@@ -1628,7 +1628,7 @@ let ssr_id_of_string loc s =
   ^ "Scripts with explicit references to anonymous variables are fragile."))
     end; Id.of_string s
 
-let ssr_null_entry = Gram.Entry.of_parser "ssr_null" (fun _ -> ())
+let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ -> ())
 
 }
 
@@ -1955,7 +1955,7 @@ let accept_ssreqid strm =
                       accept_before_syms [":"] strm
   | _ -> raise Stream.Failure
 
-let test_ssreqid = Gram.Entry.of_parser "test_ssreqid" accept_ssreqid
+let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid
 
 }
 
@@ -2373,7 +2373,7 @@ let test_ssr_rw_syntax =
     match Util.stream_nth 0 strm with
     | Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> ()
     | _ -> raise Stream.Failure in
-  Gram.Entry.of_parser "test_ssr_rw_syntax" test
+  Pcoq.Entry.of_parser "test_ssr_rw_syntax" test
 
 }
 
@@ -2583,7 +2583,7 @@ let accept_idcomma strm =
   | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm
   | _ -> raise Stream.Failure
 
-let test_idcomma = Gram.Entry.of_parser "test_idcomma" accept_idcomma
+let test_idcomma = Pcoq.Entry.of_parser "test_idcomma" accept_idcomma
 
 }
 
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 0dd17dfc15..4ddaeb49fd 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -68,7 +68,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "(" -> '('
   | Tok.KEYWORD "@" -> '@'
   | _ -> ' '
-let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 }