The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I remember having reported a bug a long time ago.
https://coq.inria.fr/bugs/show_bug.cgi?id=2243
I do not know if it is solved now. If not you might exploit it for inductives.

2015-02-16 0:11 GMT+01:00 Jonathan Leivent <jonikelee AT gmail.com>:

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