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/funind/g_indfun.ml4 | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

(limited to 'plugins/funind')

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