The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

What aspect of the definition of [sig] in the standard library results in its first parameter being implicit.

Here's how it's defined:

Inductive sig (A:Type) (P:A -> Prop) : Type :=

    exist : forall x:A, P x -> sig A P.

[A] is not implicit here.

Later on the definition includes this:

Arguments sig (A P)%type.

Now when using the standard library, I have to leave out the value of [A].

However, if I write my own re-implementation as follows, I still have to provide an explicit value for [A].

Module foo.

Inductive sig (A:Type) (P:A -> Prop) : Type :=

    exist : forall x:A, P x -> sig A P.

Arguments sig (A P)%type.

Definition any_bp := sig  dnabasepair (fun p: dnabasepair => True).

(* I have to explicitly provide the first [dnabasepair] parameter *)

End foo.

I know this is an elementary question on implicit parameters. I read the manual but didn't find the detail I need to understand what's going on here. Thanks.