diff options
| author |  Armaël Guéneau <armael.gueneau@ens-lyon.fr> | 2018-05-31 14:17:39 +0200 |
|---|---|---|
| committer | Armaël Guéneau <armael.gueneau@ens-lyon.fr> | 2018-05-31 14:17:39 +0200 |
| commit | 852e6f960d3fc6d4cf702ab21cfe813d9edbb531 (patch) | |
| tree | ecbfed9a6840ad8e908bedcf34522968f6408eba /vernac/ppvernac.ml | |
| parent | ac8a84e3b4dc530b000e17b72c7e26f7a957420f (diff) | |
Refactor parsing rules for Hint Resolve -> and Hint Resolve <-
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 3655947a5..c2dc59065 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -200,6 +200,9 @@ open Pputils keyword "Resolve " ++ prlist_with_sep sep (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info) l + | HintsResolveIFF (l2r, l, n) -> + keyword "Resolve " ++ str (if l2r then "->" else "<-") + ++ prlist_with_sep sep pr_reference l | HintsImmediate l -> keyword "Immediate" ++ spc() ++ prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l |