Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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 _).


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




Archive powered by MHonArc 2.6.18.

Top of Page