coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] differentiate hyps from section vars

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] differentiate hyps from section vars
Date: Sun, 15 Feb 2015 18:11:06 -0500

Is there any way to tactically differentiate hypotheses that are section vars from those that are not? For instance, I'd like to revert all non-section vars without reverting any section vars. I noticed that [is_var H] is true for all hyps, whether or not they are section vars.

-- Jonathan

[Coq-Club] differentiate hyps from section vars, Jonathan Leivent, 02/16/2015
- Re: [Coq-Club] differentiate hyps from section vars, Cedric Auger, 02/16/2015
  - Re: [Coq-Club] differentiate hyps from section vars, Pierre-Marie Pédrot, 02/16/2015
    - Re: [Coq-Club] differentiate hyps from section vars, Pierre-Marie Pédrot, 02/16/2015
      - Re: [Coq-Club] differentiate hyps from section vars, Jonathan Leivent, 02/16/2015