diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-04 17:03:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-04 17:04:27 +0100 |
| commit | 94bdd90bacc4d4a92b79bbe0db532e523fbcbce8 (patch) | |
| tree | ebc0238c23aa76190e26f2598ffddbaf338276a0 /test-suite | |
| parent | 22dfbff296cf03b6fab2bcec4eb5f9cf6ee8368c (diff) | |
Test for #4966 ("auto" wrongly seen as "auto with *" when in position of ident).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4966.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4966.v b/test-suite/bugs/closed/4966.v new file mode 100644 index 000000000..bd93cdc85 --- /dev/null +++ b/test-suite/bugs/closed/4966.v @@ -0,0 +1,10 @@ +(* Interpretation of auto as an argument of an ltac function (i.e. as an ident) was wrongly "auto with *" *) + +Axiom proof_admitted : False. +Hint Extern 0 => case proof_admitted : unused. +Ltac do_tac tac := tac. + +Goal False. + Set Ltac Profiling. + Fail solve [ do_tac auto ]. +Abort. |