diff options
Diffstat (limited to 'grammar/vernacextend.ml4')
| -rw-r--r-- | grammar/vernacextend.ml4 | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 57079fccd..3bb1e0907 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -35,7 +35,6 @@ type rule = { let rec make_let e = function | [] -> e | ExtNonTerminal (t, _, p) :: l -> - let p = Names.Id.to_string p in let loc = MLast.loc_of_expr e in let e = make_let e l in <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> @@ -49,7 +48,7 @@ let make_clause { r_patt = pt; r_branch = e; } = (* To avoid warnings *) let mk_ignore c pt = let names = CList.map_filter (function - | ExtNonTerminal (_, _, p) -> Some (Names.Id.to_string p) + | ExtNonTerminal (_, _, p) -> Some p | _ -> None) pt in let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in let names = List.fold_left fold <:expr< () >> names in @@ -181,10 +180,10 @@ EXTEND args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) + ExtNonTerminal (type_of_user_symbol e, e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) + ExtNonTerminal (type_of_user_symbol e, e, s) | s = STRING -> ExtTerminal s ] ] |