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.

2 files changed, 16 insertions, 20 deletions

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