coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] making a proof done with assert transparent
- Date: Mon, 12 Oct 2015 12:11:47 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f169.google.com
- Ironport-phdr: 9a23:DQFRkBYsBqhcTDD6uAuCQsv/LSx+4OfEezUN459isYplN5qZpci9bnLW6fgltlLVR4KTs6sC0LqK9fC6Ej1aqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7z0q8eYMl8ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksezQ+49Suvh3eRyOO4GEdWyMYiEwbLRLC6UTYV4z2tGPVrO1mw2HOP8TtSrY7QzO59PZDRxrhiSNBPDk8pjKEwvdshb5W9Ury7yd0xJTZNdmY
As suggested in the bug report, you can try something like:
Tactic Notation "transparent" "assert" "(" ident(H) ":" uconstr(type) ")" :=
refine (let H := (_ : type) in _).
Tactic Notation "transparent" "assert" "(" ident(H) ":" uconstr(type) ")" :=
refine (let H := (_ : type) in _).
On Mon, Oct 12, 2015 at 10:30 AM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:
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, Daniel de Rauglaudre, 10/13/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, Soegtrop, Michael, 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, 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
Archive powered by MHonArc 2.6.18.