[yegor] 1.Coq uses same rules for statements of the form _T_ and _t in T_, we had to add some extra rules to support it, which finally brought extracts into the theory._ Fri Aug 31 09:38:16 PDT 2007 http://svn.metaprl.org/commitlogs/metaprl/2007-08/2007-08-31-09-38-16-638872000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2007-08/2007-08-31-09-38-16-638872000-PDT.html