The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi everyone,

  I think the best you can do in the current state is to manipulate
an existential variable for the object explicitely using an encoding 
like:

Inductive singleton A : A -> Type := single (x : A) : singleton A x.

Implicit Arguments single [[A]].

Ltac assert_trans x T :=
  evar (x:T); let H := fresh in assert (H:singleton T x); [unfold x; clear 
x|clear H]. 

Lemma singleton_apply {A B} (f : A -> B) (x : A) : singleton A x -> singleton 
B (f x).
Proof. intros. destruct X. constructor; auto. Defined.

Goal forall x : nat, True.
intros.
assert_trans foo bool.
(* now in a [singleton bool ?n] goal where we can refine ?n].
apply (singleton_apply negb). 
apply (single true).
(* foo := negb true is in the context *)
exact I.
Qed.

It's a hack and doesn't support directly using a tactic to build the term, 
but at least
you get the transparency you need.

My 2 cents,
-- Matthieu

Le 7 avr. 2010 à 11:03, Pierre Courtieu a écrit :

> Yes that's right. You can only see its definition but you cannot make
> it transparent.
> P.
> 
> Le 7 avril 2010 15:51, Pierre-Marie Pédrot
>Â <pierremarie.pedrot AT ens-lyon.fr>
>  a écrit :
>> Technically, it does not work as the term produced through abstract is
>> opaque, so we end up with the very same problem as assert.
>> 
>> PMP
>