diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 796636c0e..32a2427ed 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -105,7 +105,8 @@ GEXTEND Gram [ [ IDENT "Local" -> true | -> false ] ] ; hint: - [ [ IDENT "Resolve"; lc = LIST1 constr -> HintsResolve lc + [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] -> + HintsResolve (List.map (fun x -> (n, x)) lc) | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc |