diff options
Diffstat (limited to 'grammar/tacextend.ml4')
| -rw-r--r-- | grammar/tacextend.ml4 | 23 |
1 files changed, 18 insertions, 5 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index e52770aa2..19b6e1b5f 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -45,13 +45,26 @@ let make_fun_clauses loc s l = let map c = Compat.make_fun loc [make_clause c] in mlexpr_of_list map l +let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >> + +let rec mlexpr_of_symbol = function +| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >> +| Uentry e -> + let arg = get_argt <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> +| Uentryl (e, l) -> + assert (e = "tactic"); + let arg = get_argt <:expr< Constrarg.wit_tactic >> in + <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> + let make_prod_item = function - | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> + | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> | ExtNonTerminal (g, id) -> - let nt = type_of_user_symbol g in - let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in - <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ - $mlexpr_of_prod_entry_key base g$ >> + <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >> let mlexpr_of_clause cl = mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl |