The Coq mailing list

[Nada Amin <namin AT alum.mit.edu>]

Hi,

There is such a tactic called skip in the library of Software Foundations.
See http://www.cis.upenn.edu/~bcpierce/sf/LibTactics.html#lab809
and http://www.cis.upenn.edu/~bcpierce/sf/UseTactics.html#lab828

Cheers,
~n

On Wed, Mar 7, 2012 at 1:08 PM, Paolo Herms 
<paolo.herms AT cea.fr>
 wrote:
> Hello,
> is there a tactic that like "admit" discharges the current subgoal by
> admitting it, but instead of stating it as global axiom it would state a
> hypothesis local to the current section?
> If not would it be possible to make one in a plugin or do you see any
> technical difficulties?
> I'm thinking such a tactic would allow to define generic proof schemes in a
> flexible way.
> Any remarks are appreciated.
> Thanks,
> --
> Paolo Herms
> PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
> Paris, France
>
>