From bb4daa4af0515f3041203c5bcc0a1d8cd1123e5a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 22 Nov 2018 11:40:57 +0100
Subject: Only use Coq API in coqpp.

---
 coqpp/coqpp_main.ml                   | 10 +++++-----
 parsing/g_prim.mlg                    |  1 -
 plugins/ltac/g_rewrite.mlg            |  2 --
 plugins/ssrmatching/g_ssrmatching.mlg |  1 -
 4 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 8da4c6db13..d52bd39d72 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -139,7 +139,7 @@ let print_local fmt ext =
   match locals with
   | [] -> ()
   | e :: locals ->
-    let mk_e fmt e = fprintf fmt "%s.Entry.create \"%s\"" ext.gramext_name e in
+    let mk_e fmt e = fprintf fmt "Pcoq.Entry.create \"%s\"" e in
     let () = fprintf fmt "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in
     let iter e = fprintf fmt "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in
     let () = List.iter iter locals in
@@ -277,16 +277,16 @@ let print_rule fmt r =
   let pr_prd fmt prd = print_list fmt print_prod prd in
   fprintf fmt "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods)
 
-let print_entry fmt gram e =
+let print_entry fmt e =
   let print_position_opt fmt pos = print_opt fmt print_position pos in
   let print_rules fmt rules = print_list fmt print_rule rules in
-  fprintf fmt "let () =@ @[%s.gram_extend@ %s@ @[(%a, %a)@]@]@ in@ "
-    gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
+  fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ None@ @[(%a, %a)@]@]@ in@ "
+    e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
 
 let print_ast fmt ext =
   let () = fprintf fmt "let _ = @[" in
   let () = fprintf fmt "@[<v>%a@]" print_local ext in
-  let () = List.iter (fun e -> print_entry fmt ext.gramext_name e) ext.gramext_entries in
+  let () = List.iter (fun e -> print_entry fmt e) ext.gramext_entries in
   let () = fprintf fmt "()@]@\n" in
   ()
 
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index dfb788907e..6247a12640 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -13,7 +13,6 @@
 open Names
 open Libnames
 
-open Pcoq
 open Pcoq.Prim
 
 let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 2596bc22f2..f7375a0f01 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -226,8 +226,6 @@ let () =
   let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in
   Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer
 
-open Pcoq
-
 }
 
 GRAMMAR EXTEND Gram
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 3f0794fdd4..0dd17dfc15 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -11,7 +11,6 @@
 {
 
 open Ltac_plugin
-open Pcoq
 open Pcoq.Constr
 open Ssrmatching
 open Ssrmatching.Internal
-- 
cgit v1.2.3