coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)

From: Jonathan <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)
Date: Tue, 22 Jul 2014 22:36:21 -0400

On 07/22/2014 07:18 PM, Jason Gross wrote:

I believe [instantiate] is unofficially deprecated in trunk. I generally
prefer to handle evars manually, rather than by number, but, *shrugs*

Instantiate deprecated? I thought that was the way to handle evars manually. How else?

[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