The Coq mailing list

[Lo�c Pottier <Loic.Pottier AT sophia.inria.fr>]

Sorry, it's wrong...

So the problem remains.

 

Loïc

----- Original Message -----

From: Loïc Pottier

To: Loïc Pottier ; coq-club AT pauillac.inria.fr

Sent: Friday, November 12, 2004 11:58 AM

Subject: Re: [Coq-Club] name of binded variables

Hi,

I found a "stone age" solution to my problem:

 

Ltac elimex h :=
  let th:= type of h in
  let h1:=fresh "H" in
  match th with
    | (ex_T _ (fun x:_ => _)) => let v:=fresh "x" in (generalize h;clear h; intros (v,h1))
    | (ex_T _ (fun l:_ => _)) => let v:=fresh "l" in (generalize h;clear h; intros (v,h1))
    | (ex_T _ (fun eta:_ => _)) => let v:=fresh "eta" in (generalize h;clear h; intros (v,h1))

    ...

  end.

 

Loïc

----- Original Message -----

From: Loïc Pottier

To: coq-club AT pauillac.inria.fr

Sent: Monday, November 08, 2004 9:36 AM

Subject: [Coq-Club] name of binded variables

 

Hi,

 I have a goal

 

H: ex_T R (fun eta:R => P eta)

======================

...

 

with

 

elim H; intros

 

the name of the existemtial variable eta is forgotten and replaced with x!

 

How to keep trace of this name and obtain a goal:

 

eta:R

H0: P eta

==========================

...

 

???

 

Loïc