# Documentation of \`{!Foo}?

**URL:** <https://discourse.rocq-prover.org/t/documentation-of-foo/129>\
**Category:** Using Rocq\
**Created:** [February 22, 2019, 2:41pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129 "2019-02-22T14:41:54Z")\
**Posts on this page:** 6\
**Page:** 2

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [May 24, 2019, 8:25pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/21 "2019-05-24T20:25:48Z")

</div>

Isn’t it already what’s meant by this paragraph?

> When generalizing a binder whose type is a typeclass, its own class arguments are omitted from the syntax and are generalized using automatic names, without instance search. Other arguments are also generalized unless provided.

and reinforced by:

> this behaviour may be disabled by prefixing the type with a `!` or by forcing the typeclass name to be an explicit application using `@` (however the later ignores implicit argument information).

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [May 25, 2019, 9:58am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/22 "2019-05-25T09:58:40Z")

</div>

Where does that say that this ignores the implicit status of arguments? See for example

```coq
Class tc_def2 {H:False} := mkDef2 : Type.

Generalizable All Variables.
Section test.
Context `{tc_def2 X}. (* implicit argument became explicit?? *)

```

I would expect this to error because `tc_def2`'s only argument is implicit. But this gets accepted.

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [May 25, 2019, 1:16pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/23 "2019-05-25T13:16:46Z")

</div>

Alright, I had misunderstood what you meant. This is weird indeed, and looks like a bug.

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [May 28, 2019, 4:10pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/24 "2019-05-28T16:10:13Z")

</div>

@SkySkimmer do you agree that this is a bug? Should I open an issue?

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [May 28, 2019, 4:22pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/25 "2019-05-28T16:22:08Z")

</div>

Maybe a documentation bug, I don’t know if there’s a sensible way to handle implicits together with the rest of the feature.

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [May 29, 2019, 8:17am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/26 "2019-05-29T08:17:26Z")

</div>

[Reported a bug](https://github.com/coq/coq/issues/10272)

[Previous page](https://discourse.rocq-prover.org/t/documentation-of-foo/129.md?page=1)