diff options
| -rw-r--r-- | parsing/g_proofs.ml4 | 2 | ||||
| -rw-r--r-- | test-suite/success/Hints.v | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 78294f2a71..9f5ef5c8be 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -90,7 +90,7 @@ GEXTEND Gram id = ident; hyptyp = Constr.constr_pattern; pri = natural; - tac = tactic -> + "["; tac = tactic; "]" -> VernacHintDestruct (id,dloc,hyptyp,pri,tac) | IDENT "Hint"; hintname = ident; dbnames = opt_hintbases; ":="; h = hint diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 036ba034dd..f32753e023 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -17,9 +17,9 @@ Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal. Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal : foo. (* What's this stranged syntax ? *) -HintDestruct Conclusion h6 (le ? ?) 4 [ (Apply $0) ]. -HintDestruct Discardable Hypothesis h7 (le ? ?) 4 [ (Apply $0) ]. -HintDestruct Hypothesis h8 (le ? ?) 4 [ (Apply $0) ]. +HintDestruct Conclusion h6 (le ? ?) 4 [ Fun H -> Apply H ]. +HintDestruct Discardable Hypothesis h7 (le ? ?) 4 [ Fun H -> Apply H ]. +HintDestruct Hypothesis h8 (le ? ?) 4 [ Fun H -> Apply H ]. (* Checks that local names are accepted *) Section A. |