coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] making a proof done with assert transparent
Date: Mon, 12 Oct 2015 14:30:26 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
Ironport-phdr: 9a23:vuieKR2cEvE5zGU3smDT+DRfVm0co7zxezQtwd8ZsegRK/ad9pjvdHbS+e9qxAeQG96Lt7QU0aGJ6ejJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6OyZTtnL/os7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JsKWqLjOq88ULZwDTI8Mmlz6teh/U3IShLK7X8BWE0XlABJCk7L9kepcI32t36wje1w1zWAOtWyBZU1UjSr4qMhAEvtiSwHPjM9tnrQh8NslqVDiBOnuxF7hYXTZdfGZ7JFYqrBcIZCFiJ6VcFLWnkZDw==

Dear Pierre,

actually the 8.5 manual is accessible online:

Main entry:

https://coq.inria.fr/distrib/V8.5beta2/refman/

Unshelve:

https://coq.inria.fr/distrib/V8.5beta2/refman/Reference-Manual010.html#unshelve

Best regards,

Michael

-----Original Message-----
From:
pierre.courtieu AT gmail.com

[mailto:pierre.courtieu AT gmail.com]
On Behalf Of Pierre Courtieu
Sent: Monday, October 12, 2015 2:54 PM
To: Coq Club
Subject: Re: [Coq-Club] making a proof done with assert transparent

Actually Unshelve is documented in v8.5 (which is not on coq web site). It is
a command, not a tactic.

For the record "swap" can be used to change the ordering of goals:

eval(foo : bar).
Unshelve.
all:swap 1 2.

But I guess other solutions with only tactics are better.

P.
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[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