diff options
| author | Matthieu Sozeau | 2014-09-15 21:33:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-15 21:37:31 +0200 |
| commit | 62a552b508b747b6cdf4bd818233f001ae4ce555 (patch) | |
| tree | 80feb19c8d02935b550c7f6c971ea42fc39020b2 /parsing | |
| parent | 1c113305039857ca219f252f5e80f4b179a39082 (diff) | |
Add a "Hint Mode ref (+ | -)*" hint for setting a global mode
of resulution for goals whose head is "ref". + means the argument
is an input and shouldn't contain an evar, otherwise resolution
fails. This generalizes the Typeclasses Strict Resolution option
which prevents resolution to fire on underconstrained typeclass
constraints, now the criterion can be applied to specific parameters.
Also cleanup auto/eauto code, uncovering a potential backwards
compatibility issue: in cases the goal contains existentials, we
never use the discrimination net in auto/eauto. We should try to
set this on once the contribs are stabilized (the stdlib goes through
when the dnet is used in these cases).
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 212d4af6d9..2c8eb85b80 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -146,6 +146,7 @@ GEXTEND Gram | 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) + | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m) | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; @@ -156,4 +157,7 @@ GEXTEND Gram [ [ ":="; c = lconstr -> c | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ] ; + mode: + [ [ l = LIST1 ["+" -> true | "-" -> false] -> l ] ] + ; END |