diff options
Diffstat (limited to 'grammar/vernacextend.ml4')
| -rw-r--r-- | grammar/vernacextend.ml4 | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 453907689..40e327c37 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -43,9 +43,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 +101,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 +164,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 ; "]" ; |