A way to specialize universally quantified hypothesis: if H is

   H: forall (n:nat)(b:bool), P n b 
then "narrow H with 0 true" will leave H: P 0 true. 

The name for this tactic should ideally be "specialize", but this one
already exists (old stuff, same idea but no "in place" modification, 
not documented anymore, still used in users contribs). 





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10283 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions