The Coq mailing list

["Brian E. Aydemir" <baydemir AT cis.upenn.edu>]

Quoting Thorsten Altenkirch 
<txa AT Cs.Nott.AC.UK>:

> for my lecture I'd like to use sums (i.e. coproducts) so that both  
> arguments of injections are inferred. Set Implicit Contextual  
> doesn't seem to do the trick. Is there a way?
>
> Set Contextual Implicit.
> Definition ex2 : nat + bool := inl  black.

If nothing else, you can use Implicit Arguments to explicitly declare  
the implicit arguments for a constant:

Implicit Arguments inl [A B].
Implicit Arguments inr [A B].
Definition ex2 : nat + bool := inl  black.  (* assuming black : nat *)

Hope that helps,
Brian