coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)
- Date: Wed, 23 Jul 2014 14:38:02 +0200
Make sure you have decent alternatives for all current uses of
"instantiate" before your sense of elegance takes over. Thanks in
advance.
I doubt it's reasonable to even consider removing [instantiate] from Ltac in the foreseeable future. I didn't mean to imply it would be. My hope is, rather, that better solutions will be found with the new mechanism. I must say that you are right, though: [erewrite] is rather thorny.
- [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/22/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/22/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/22/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Xavier Leroy, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- [Coq-Club] nice evar tactics (was: Re: Prop smuggling (was: Re: Smart case analysis in Coq.)), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/24/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Xavier Leroy, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Arnaud Spiwack, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/23/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jonathan, 07/22/2014
- Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.), Jason Gross, 07/22/2014
Archive powered by MHonArc 2.6.18.