The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

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