diff options
Diffstat (limited to 'grammar/vernacextend.ml4')
| -rw-r--r-- | grammar/vernacextend.ml4 | 27 |
1 files changed, 16 insertions, 11 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 453907689e..aedaead71a 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -30,7 +30,8 @@ type rule = { let rec make_let e = function | [] -> e - | ExtNonTerminal (t, _, p) :: l -> + | ExtNonTerminal (g, p) :: l -> + let t = type_of_user_symbol g 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$ >> @@ -43,9 +44,11 @@ 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 p - | _ -> None) pt in + let fold accu = function + | ExtNonTerminal (_, p) -> p :: accu + | _ -> accu + in + let names = List.fold_left fold [] pt in let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in let names = List.fold_left fold <:expr< () >> names in <:expr< do { let _ = $names$ in $c$ } >> @@ -99,10 +102,12 @@ let make_fun_classifiers loc s c l = let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in mlexpr_of_list (fun x -> x) cl -let mlexpr_of_clause = - mlexpr_of_list - (fun { r_head = a; r_patt = b; } -> mlexpr_of_list make_prod_item - (Option.List.cons (Option.map (fun a -> ExtTerminal a) a) b)) +let mlexpr_of_clause cl = + let mkexpr { r_head = a; r_patt = b; } = match a with + | None -> mlexpr_of_list make_prod_item b + | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b) + in + mlexpr_of_list mkexpr cl let declare_command loc s c nt cl = let se = mlexpr_of_string s in @@ -160,7 +165,7 @@ EXTEND rule: [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let () = if CString.is_empty s then failwith "Command name is empty." in + let () = if s = "" then failwith "Command name is empty." in let b = <:expr< fun () -> $e$ >> in { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } | "[" ; "-" ; l = LIST1 args ; "]" ; @@ -175,10 +180,10 @@ EXTEND args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (type_of_user_symbol e, e, s) + ExtNonTerminal (e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (type_of_user_symbol e, e, s) + ExtNonTerminal (e, s) | s = STRING -> ExtTerminal s ] ] |