diff options
Diffstat (limited to 'grammar/tacextend.mlp')
| -rw-r--r-- | grammar/tacextend.mlp | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index b14fba975..3057ee58c 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -31,19 +31,19 @@ let mlexpr_of_ident id = let rec make_patt = function | [] -> <:patt< [] >> - | ExtNonTerminal (_, p) :: l -> + | ExtNonTerminal (_, Some p) :: l -> <:patt< [ $lid:p$ :: $make_patt l$ ] >> | _::l -> make_patt l let rec make_let raw e = function | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> - | ExtNonTerminal (g, p) :: l -> + | ExtNonTerminal (g, Some p) :: l -> let t = type_of_user_symbol g in let loc = MLast.loc_of_expr e in let e = make_let raw e l in let v = if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >> - else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in + else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let raw e l @@ -75,7 +75,7 @@ let rec mlexpr_of_symbol = function let make_prod_item = function | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> | ExtNonTerminal (g, id) -> - <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >> + <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_option mlexpr_of_ident id$ >> let mlexpr_of_clause cl = mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl @@ -87,7 +87,7 @@ let is_constr_gram = function | _ -> false let make_var = function - | ExtNonTerminal (_, p) -> Some p + | ExtNonTerminal (_, p) -> p | _ -> assert false let declare_tactic loc tacname ~level classification clause = match clause with @@ -158,10 +158,13 @@ EXTEND tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) + | e = LIDENT -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, None) | s = STRING -> let () = if s = "" then failwith "Empty terminal." in ExtTerminal s |