From 002a974b66bc5b8524c8c045d6b9ec4f57aa7734 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 8 Nov 2018 13:17:14 +0100
Subject: [gramlib] [build] Switch make-based system to packed gramlib

This makes the make-based build system stop linking to Camlp5's
gramlib and instead links to our own gramlib.

We use the style done in the packing of `Stdlib` in OCaml 4.07.

As to introduce a minimal amount of noise in history we use an
autogenerated `gramlib__pack` directory.

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
---
 plugins/funind/plugin_base.dune      | 1 -
 plugins/ltac/plugin_base.dune        | 1 -
 plugins/ssr/ssrcommon.ml             | 4 ++--
 plugins/ssr/ssrelim.ml               | 2 +-
 plugins/ssrmatching/plugin_base.dune | 1 -
 5 files changed, 3 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
index 9f583234d8..002eb28eea 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/plugin_base.dune
@@ -2,5 +2,4 @@
  (name recdef_plugin)
  (public_name coq.plugins.recdef)
  (synopsis "Coq's functional induction plugin")
- (flags :standard -open Gramlib)
  (libraries coq.plugins.extraction))
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
index 1b31655310..5611f5ba16 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/plugin_base.dune
@@ -3,7 +3,6 @@
  (public_name coq.plugins.ltac)
  (synopsis "Coq's LTAC tactic language")
  (modules :standard \ tauto)
- (flags :standard -open Gramlib)
  (libraries coq.stm))
 
 (library
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index fa58a1c39a..ff323ddf47 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1092,8 +1092,8 @@ let tclDO n tac =
         let _, info = CErrors.push e in
         let e' = CErrors.UserError (l, prefix i ++ s) in
         Util.iraise (e', info)
-    | Ploc.Exc(loc, CErrors.UserError (l, s))  -> 
-        raise (Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+    | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s))  ->
+        raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
   let rec loop i gl =
     if i = n then tac_err_at i gl else
     (tclTHEN (tac_err_at i) (loop (i + 1))) gl in
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index d09b81593e..3f87ccd2bf 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -404,7 +404,7 @@ let equality_inj l b id c gl =
   let msg = ref "" in
   try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
   with
-    | Ploc.Exc(_,CErrors.UserError (_,s))
+    | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s))
     | CErrors.UserError (_,s)
   when msg := Pp.string_of_ppcmds s;
        !msg = "Not a projectable equality but a discriminable one." ||
diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune
index 1450a94de1..06f67c3774 100644
--- a/plugins/ssrmatching/plugin_base.dune
+++ b/plugins/ssrmatching/plugin_base.dune
@@ -2,5 +2,4 @@
  (name ssrmatching_plugin)
  (public_name coq.plugins.ssrmatching)
  (synopsis "Coq ssrmatching plugin")
- (flags :standard -open Gramlib)
  (libraries coq.plugins.ltac))
-- 
cgit v1.2.3