coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] making a proof done with assert transparent

From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] making a proof done with assert transparent
Date: Mon, 12 Oct 2015 14:10:23 +0200

Ah, Unshelve, ok. Seems not to be in the documentation. I see it works
but if I want to prove it immediately, I must use "Focus" after.

Otherwise, the solution with refine given here seems to work also.
But both solutions are not clear for the reader. An "assert" with
option "transparent" would be good :-)

On Mon, Oct 12, 2015 at 01:49:58PM +0200, Pierre Courtieu wrote:
> Hi Daniel, I think "Unshelve." is what your are looking for.

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

[Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre Courtieu, 10/12/2015
  - Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015
    - Re: [Coq-Club] making a proof done with assert transparent, Pierre Courtieu, 10/12/2015
      - RE: [Coq-Club] making a proof done with assert transparent, Soegtrop, Michael, 10/12/2015
        
        Re: [Coq-Club] making a proof done with assert transparent, Jason Gross, 10/12/2015
        
        Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/13/2015
        
        Re: [Coq-Club] making a proof done with assert transparent, Pierre-Marie Pédrot, 10/13/2015
        Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/13/2015
- Re: [Coq-Club] making a proof done with assert transparent, Ilmārs Cīrulis, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre-Marie Pédrot, 10/12/2015
  - Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015