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.

8 files changed, 53 insertions, 41 deletions

diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 34f1cf6cb6..6e491b076f 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -60,5 +60,5 @@ let rec mlexpr_of_prod_entry_key = function
   | Pcoq.Anext -> <:expr< Pcoq.Anext >>
   | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >>
   | Pcoq.Agram s -> Errors.anomaly (Pp.str "Agram not supported")
-  | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >>
+  | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.name $lid:s$) >>
   | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >>
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 *)
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 216d88e66d..fe75d17f6a 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -83,14 +83,6 @@ let vernac_proof_instr instr =
     Vernacentries.print_subgoals ()
   end
 
-(* We create a new parser entry [proof_mode]. The Declarative proof mode
-    will replace the normal parser entry for tactics with this one. *)
-let proof_mode : vernac_expr Gram.entry =
-  Gram.entry_create "vernac:proof_command"
-(* Auxiliary grammar entry. *)
-let proof_instr : raw_proof_instr Gram.entry =
-  Gram.entry_create "proofmode:instr"
-
 (* Before we can write an new toplevel command (see below) 
     which takes a [proof_instr] as argument, we need to declare
     how to parse it, print it, globalise it and interprete it.
@@ -103,6 +95,14 @@ let proof_instr : raw_proof_instr Gram.entry =
 let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type =
   Genarg.make0 None "proof_instr"
 
+(* We create a new parser entry [proof_mode]. The Declarative proof mode
+    will replace the normal parser entry for tactics with this one. *)
+let proof_mode : vernac_expr Gram.entry =
+  Gram.entry_create "vernac:proof_command"
+(* Auxiliary grammar entry. *)
+let proof_instr : raw_proof_instr Gram.entry =
+  Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr)
+
 let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
   pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 3e4f67498f..ca90b37593 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -135,13 +135,13 @@ module Gram = Pcoq.Gram
 module Vernac = Pcoq.Vernac_
 module Tactic = Pcoq.Tactic
 
-module FunctionGram =
-struct
-  let gec s = Gram.entry_create ("Function."^s)
-		(* types *)
-  let function_rec_definition_loc : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located Gram.entry = gec "function_rec_definition_loc"
-end
-open FunctionGram
+type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
+
+let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
+  Genarg.create_arg None "function_rec_definition_loc"
+
+let function_rec_definition_loc =
+  Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
 
 GEXTEND Gram
   GLOBAL: function_rec_definition_loc ;
@@ -150,11 +150,7 @@ GEXTEND Gram
     [ [ g = Vernac.rec_definition -> !@loc, g ]]
     ;
 
-  END
-type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
-
-let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
-  Genarg.create_arg None "function_rec_definition_loc"
+END
 
 (* TASSI: n'importe quoi ! *)
 VERNAC COMMAND EXTEND Function
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index db98c42503..03bbc4b046 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -25,7 +25,6 @@ open Tacmach
 open Tacticals
 open Tactics
 open Rewrite
-open Pcoq.Constr
 
 type constr_expr_with_bindings = constr_expr with_bindings
 type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
@@ -200,6 +199,16 @@ type binders_argtype = local_binder list
 let wit_binders =
  (Genarg.create_arg None "binders" : binders_argtype Genarg.uniform_genarg_type)
 
+let binders = Pcoq.create_generic_entry "binders" (Genarg.rawwit wit_binders)
+
+open Pcoq
+
+GEXTEND Gram
+  GLOBAL: binders;
+    binders:
+    [ [ b = Pcoq.Constr.binders -> b ] ];
+END
+
 VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)