Removing non-marshallable data from the Agram constructor. Instead of

containing opaque grammar objects, it now contains a string representing
the entry. In order to recover the entry from the string, the former must
have been created with [Pcoq.create_generic_entry] or similar. This is
guaranteed for entries generated by ARGUMENT EXTEND, and must be done by
hand otherwise.

Some plugins were fixed accordingly.

4 files changed, 26 insertions, 19 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index d405de921f..9aa417a094 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -363,7 +363,7 @@ let create_ltac_quotation name cast wit e =
   let rule = [
     gram_token_of_string name;
     gram_token_of_string ":";
-    symbol_of_prod_entry_key (Agram (Gram.Entry.obj e));
+    symbol_of_prod_entry_key (Agram (Gram.Entry.name e));
   ] in
   let action v _ _ loc =
     let loc = !@loc in
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index fe024d409d..2354aa3325 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -25,18 +25,17 @@ module Gram = Pcoq.Gram
 module Vernac = Pcoq.Vernac_
 module Tactic = Pcoq.Tactic
 
-module ObligationsGram =
-struct
-  let gec s = Gram.entry_create s
-
-  let withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "withtac"
-end
-
-open ObligationsGram
 open Pcoq
 
 let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
+type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
+
+let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
+  Genarg.create_arg None "withtac"
+
+let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac)
+
 GEXTEND Gram
   GLOBAL: withtac;
 
@@ -53,11 +52,6 @@ GEXTEND Gram
 
   END
 
-type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
-
-let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
-  Genarg.create_arg None "withtac"
-
 open Obligations
 
 let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index e26ecbea34..6dee6cf160 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -80,7 +80,7 @@ type prod_entry_key =
   | Aself
   | Anext
   | Atactic of int
-  | Agram of G.internal_entry
+  | Agram of string
   | Aentry of string * string
 
 (** [grammar_object] is the superclass of all grammar entries *)
@@ -729,10 +729,23 @@ let rec symbol_of_prod_entry_key = function
   | Atactic 5 -> Snterm (Gram.Entry.obj Tactic.binder_tactic)
   | Atactic n ->
       Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n)
-  | Agram s -> Snterm s
+  | Agram s ->
+    let e =
+      try
+      (** ppedrot: we should always generate Agram entries which have already
+          been registered, so this should not fail. *)
+        let (u, s) = match String.split ':' s with
+        | u :: s :: [] -> (u, s)
+        | _ -> raise Not_found
+        in
+        get_entry (get_univ u) s
+      with Not_found ->
+        Errors.anomaly (str "Unregistered grammar entry: " ++ str s)
+    in
+    Snterm (Gram.Entry.obj (object_of_typed_entry e))
   | Aentry (u,s) ->
-      Snterm (Gram.Entry.obj
-	(object_of_typed_entry (get_entry (get_univ u) s)))
+    let e = get_entry (get_univ u) s in
+    Snterm (Gram.Entry.obj (object_of_typed_entry e))
 
 let level_of_snterml = function
   | Snterml (_,l) -> int_of_string l
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 56282f2f67..5dcfa844a4 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -272,7 +272,7 @@ type prod_entry_key =
   | Aself
   | Anext
   | Atactic of int
-  | Agram of Gram.internal_entry
+  | Agram of string
   | Aentry of string * string
 
 (** Binding general entry keys to symbols *)