coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Burak Ekici <burak-ekici AT uiowa.edu>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] a tactic replacing "Grab Existential Variables" vernac.
Date: Fri, 4 Nov 2016 19:58:59 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=burak-ekici AT uiowa.edu; spf=None smtp.mailfrom=burak-ekici AT uiowa.edu; spf=Pass smtp.helo=postmaster AT NAM03-CO1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:LFO73BwHyKs8CKrXCy+O+j09IxM/srCxBDY+r6Qd0u0VIJqq85mqBkHD//Il1AaPBtSBraMcwLCJ++C4ACpbvsbH6ChDOLV3FDY7yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9dazJHduGhMOukuu25pf7YgNShTP7b6kkfzusqgCEnNQMiIgqB6UwwRqB9nFVYe1VgG5rJFmStwv94di5upNv7nID6Loa68dcXPCiLOwDRrtCAWF+Pg==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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