From abd83cffe1afe6745775c67b8c827038e295a1d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Feb 2014 04:17:30 +0100
Subject: 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.
---
 plugins/decl_mode/g_decl_mode.ml4 | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'plugins/decl_mode')

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
 
-- 
cgit v1.2.3