diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_proofs.ml4 | 13 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 3 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 1 |
3 files changed, 9 insertions, 8 deletions
diff --git a/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4 index 56229c765..a3806ff68 100644 --- a/vernac/g_proofs.ml4 +++ b/vernac/g_proofs.ml4 @@ -98,15 +98,8 @@ GEXTEND Gram VernacCreateHintDb (id, b) | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> VernacRemoveHints (dbnames, ids) - | IDENT "Hint"; h = hint; - dbnames = opt_hintbases -> + | IDENT "Hint"; h = hint; dbnames = opt_hintbases -> VernacHints (dbnames, h) - (* Declare "Resolve" explicitly so as to be able to later extend with - "Resolve ->" and "Resolve <-" *) - | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; - info = hint_info; dbnames = opt_hintbases -> - VernacHints (dbnames, - HintsResolve (List.map (fun x -> (info, true, x)) lc)) ] ]; reference_or_constr: [ [ r = global -> HintsReference r @@ -115,6 +108,10 @@ GEXTEND Gram hint: [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> HintsResolve (List.map (fun x -> (info, true, x)) lc) + | IDENT "Resolve"; "->"; lc = LIST1 global; n = OPT natural -> + HintsResolveIFF (true, lc, n) + | IDENT "Resolve"; "<-"; lc = LIST1 global; n = OPT natural -> + HintsResolveIFF (false, lc, n) | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 7aff758e9..5490b9ce5 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 diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index fb40f0d9c..9e8dfc4f8 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -124,6 +124,7 @@ type hint_info_expr = Hints.hint_info_expr type hints_expr = Hints.hints_expr = | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list + | HintsResolveIFF of bool * reference list * int option | HintsImmediate of Hints.reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool |