diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-16 04:17:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-16 14:36:15 +0100 |
| commit | abd83cffe1afe6745775c67b8c827038e295a1d2 (patch) | |
| tree | 047668419f552be8e803cd6e558bae917c5d49e6 /plugins/funind/g_indfun.ml4 | |
| parent | f4d6b4bce315639008b52727f741de82e2687d7e (diff) | |
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.
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 3e4f67498..ca90b3759 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 |