diff options
| author | Pierre-Marie Pédrot | 2016-04-14 18:59:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-14 19:08:16 +0200 |
| commit | 87a81fd7e6ff6b45c76690471eb671ba4b005338 (patch) | |
| tree | 74c6322d95552effca6a9bb1b92befdd768394ea /printing | |
| parent | f0f3d650ec4fcd1644811e099f0f3f50d660a992 (diff) | |
Moving and enhancing the grammar_tactic_prod_item_expr type.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 9054ba0b67..f0548238a7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -104,12 +104,6 @@ module Make if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1)) else id - let pr_production_item = function - | TacNonTerm (loc, nt, (p, sep)) -> - let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in - str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")" - | TacTerm s -> qs s - let pr_comment pr_c = function | CommentConstr c -> pr_c c | CommentString s -> qs s |