The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Mon, 26 Oct 2009 18:40:49 +0100, Brian E. Aydemir  
<baydemir AT cis.upenn.edu> a écrit:

> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

You can also look "Set Implicit Arguments" and "Unset ..."