coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] a tactic replacing "Grab Existential Variables" vernac.
- Date: Mon, 7 Nov 2016 11:43:03 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f176.google.com
- Ironport-phdr: 9a23:MFgNvBYxp9dyc9ZqCMuFxR7/LSx+4OfEezUN459isYplN5qZpsu+bnLW6fgltlLVR4KTs6sC0LuM9fG8EjxQqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LW5/ISWaAFVjhK8Z6lzJVO4t1b/rM4T1KllLK8tyhLP6l9Fevpbw38gcVCUmRf/68O98bZs9i1Rv7Qq8MsWAvayRLgxUbENVGduCGsy/sC+7RQ=
The tactic with the closest behavior is the (introduced in 8.5) "unshelve" tactical. Given a goal such as:
Goal P.
tac1.
Grab Existential Variables.
all:tac2.
where tac1 generated the unsolved existentials, one can (usually) replace this by:
Goal P
(unshelve tac1); tac2.
However, there are some known bugs that prevent this from always working, for instance: https://coq.inria.fr/bugs/show_bug.cgi?id=4509
-- Jonathan
On 11/04/2016 08:58 PM, Burak Ekici wrote:
Hi all,
I was wondering if there is a tactic which simply does the job of "Grab Existential Variables" vernac?
Thanks!
Best;
―
Burak.
- [Coq-Club] a tactic replacing "Grab Existential Variables" vernac., Burak Ekici, 11/05/2016
- Re: [Coq-Club] a tactic replacing "Grab Existential Variables" vernac., Jonathan Leivent, 11/07/2016
Archive powered by MHonArc 2.6.18.