diff options
| author | Matthieu Sozeau | 2016-06-10 01:15:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | 98703c8247fd86deab2d82a70c22d43797e4a548 (patch) | |
| tree | f4357abeaab6a7db53419c2ed9b3c923d7d67914 /parsing | |
| parent | 2194292dbe88674fd9a606bb22f28d332f670f77 (diff) | |
Extend Hint Mode to handle the no-head-evar case
Suggested by R. Krebbers and C. Cohen, this makes modes
more applicable, by allowing to trigger resolution on partially
instantiated indices. This is a rough but fast approximation of the
pattern on which one would like instances to apply.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 422384f3dc..b0ff8b64f2 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -134,6 +134,8 @@ GEXTEND Gram | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ] ; mode: - [ [ l = LIST1 ["+" -> true | "-" -> false] -> l ] ] + [ [ l = LIST1 [ "+" -> ModeInput + | "!" -> ModeNoHeadEvar + | "-" -> ModeOutput ] -> l ] ] ; END |