diff options
Diffstat (limited to 'grammar/tacextend.ml4')
| -rw-r--r-- | grammar/tacextend.ml4 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 19b6e1b5f6..4c4ecaf732 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -18,6 +18,11 @@ let dloc = <:expr< Loc.ghost >> let plugin_name = <:expr< __coq_plugin_name >> +let mlexpr_of_ident id = + (** Workaround for badly-designed generic arguments lacking a closure *) + let id = "$" ^ id in + <:expr< Names.Id.of_string_soft $str:id$ >> + let rec make_patt = function | [] -> <:patt< [] >> | ExtNonTerminal (_, p) :: l -> |