diff options
| author | Pierre-Marie Pédrot | 2018-07-12 16:30:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-02 09:25:25 +0200 |
| commit | 389aa51f37fda1a7a8490d1b4042b881aba730df (patch) | |
| tree | 6cf820636ded03e0fb91d954af615345c35be19a /coqpp | |
| parent | 1bde8c0912ed1129e71ffe20299ac89299492ba5 (diff) | |
Pass unnamed arguments to ML macros.
This was imposing a bit of useless burden on the API for no good reason.
Diffstat (limited to 'coqpp')
| -rw-r--r-- | coqpp/coqpp_main.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index d9fff46d88..42d8528a8c 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -296,17 +296,16 @@ let rec print_symbol fmt = function let rec print_clause fmt = function | [] -> fprintf fmt "@[TyNil@]" | ExtTerminal s :: cl -> fprintf fmt "@[TyIdent (\"%s\", %a)@]" s print_clause cl -| ExtNonTerminal (g, TokNone) :: cl -> - fprintf fmt "@[TyAnonArg (%a, %a)@]" +| ExtNonTerminal (g, _) :: cl -> + fprintf fmt "@[TyArg (%a, %a)@]" print_symbol g print_clause cl -| ExtNonTerminal (g, TokName id) :: cl -> - fprintf fmt "@[TyArg (%a, \"%s\", %a)@]" - print_symbol g id print_clause cl let rec print_binders fmt = function | [] -> fprintf fmt "ist@ " -| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders fmt rem -| (ExtNonTerminal (_, TokName id)) :: rem -> +| ExtTerminal _ :: rem -> print_binders fmt rem +| ExtNonTerminal (_, TokNone) :: rem -> + fprintf fmt "_@ %a" print_binders rem +| ExtNonTerminal (_, TokName id) :: rem -> fprintf fmt "%s@ %a" id print_binders rem let print_rule fmt r = |