Skip to content

Commit

Permalink
Merge with Nijmegen:
Browse files Browse the repository at this point in the history 
 - Dramatically reduce the memory consumption of KneserLemma.v
 - Documentation tweaks


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq-contribs/trunk/Nijmegen/CoRN@518 0cf17b13-060f-0410-b1b1-c666bec9822a
  • Loading branch information
lmamane committed Oct 23, 2006
1 parent 45c8f6e commit af80963
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 10 deletions.
14 changes: 7 additions & 7 deletions doc/www/download.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,12 @@ <h1 align="center">Downloads</h1>
<h2 id="tarballs">Tarballs</h2>
<p>You can download the total formalization or just specific parts of it.</p>
<ul>
<li><a href="downloads/CoRN.tar.gz">Full System</a></li>
<li><a href="downloads/base.tar.gz">Core</a></li>
<li><a href="downloads/alghier.tar.gz">Algebraic Hierarchy</a> </li>
<li><a href="downloads/model.tar.gz">Model of the Real Numbers</a></li>
<li><a href="downloads/fta.tar.gz">Fundamental Theorem of Algebra</a></li>
<li><a href="downloads/realcalc.tar.gz">Real Calculus</a></li>
<li><a href="http://c-corn.cs.ru.nl/downloads/CoRN.tar.gz">Full System</a></li>
<li><a href="http://c-corn.cs.ru.nl/downloads/base.tar.gz">Core</a></li>
<li><a href="http://c-corn.cs.ru.nl/downloads/alghier.tar.gz">Algebraic Hierarchy</a> </li>
<li><a href="http://c-corn.cs.ru.nl/downloads/model.tar.gz">Model of the Real Numbers</a></li>
<li><a href="http://c-corn.cs.ru.nl/downloads/fta.tar.gz">Fundamental Theorem of Algebra</a></li>
<li><a href="http://c-corn.cs.ru.nl/downloads/realcalc.tar.gz">Real Calculus</a></li>
</ul>
<p>
To download the full system, just click on the first link. The partial distributions should be self-contained, e.g. you do not need to download Core in order to use Algebraic Hierarchy. After you untar the files (which will create a CoRN/ directory at the place of installation) you will find a.o. a README file which contains more detailed instructions on how to proceed. It is (unfortunately) quite likely that all will not go well, especially if you only download parts of C-CoRN; if this happens, please contact <a href="mailto:r.oconnor@cs.ru.nl">me</a>.
Expand All @@ -37,7 +37,7 @@ <h2 id="contribute">Bleeding Edge and Contributors</h2>
<ul>
<li><samp>r.oconnor@cs.ru.nl--Nijmegen/CoRN--mainline--0</samp> located
at
<samp>http://www.cs.ru.nl/fnds-arch/roconnor/Nijmegen</samp></li>
<samp>http://www.fnds.cs.ru.nl/fnds-arch/roconnor/Nijmegen</samp></li>
</ul>
Note that the GNU Arch business is still somewhat in flux. Expect
the official mainline branch to move soonish. We might even use
Expand Down
7 changes: 4 additions & 3 deletions doc/www/info.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,12 @@ <h1 align="center">Contact Information</h1>
<ul>
<li>Project Coordinators: <a href="mailto:henk@cs.ru.nl">Henk Barendregt</a>
and <a href="mailto:herman@cs.ru.nl">Herman Geuvers</a></li>
<li>Scripts &amp; Documentation: <a href="mailto:freek@cs.ru.nl">Freek Wiedijk</a></li>
<li>Algebraic Hierarchy: <a href="mailto:lcf@cs.ru.nl">Lu&iacute;s Cruz-Filipe</a></li>
<li>Scripts: <a href="mailto:lionelm@cs.ru.nl">Lionel Mamane</a></li>
<li>Documentation: <a href="mailto:r.oconnor@cs.ru.nl">Russell O&rsquo;Connor</a></li>
<li>Algebraic Hierarchy: <a href="mailto:r.oconnor@cs.ru.nl">Russell O&rsquo;Connor</a></li>
<li>Model of the Real Numbers: <a href="mailto:milad@cs.ru.nl">Milad Niqui</a></li>
<li>Fundamental Theorem of Algebra: <a href="mailto:freek@cs.ru.nl">Freek Wiedijk</a></li>
<li>Real Calculus: Lu&iacute;s Cruz-Filipe</li>
<li>Real Calculus: <a href="mailto:lcf@cs.ru.nl">Lu&iacute;s Cruz-Filipe</a></li>
</ul>
<p>
Feel free to subscribe to the <a href="http://mailman.science.ru.nl/mailman/listinfo/C-CoRN/">
Expand Down
2 changes: 2 additions & 0 deletions fta/KneserLemma.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -328,6 +328,8 @@ astepl
cc_IR (a k[/] AbsCC b_0'[//]H7) [*] (b_0'[/] b k[//]H10)).
astepl (Zero[-]cc_IR (a k[/] AbsCC b_0'[//]H7) [*] (b_0'[/] b k[//]H10)).
astepl ( [--] (cc_IR (a k[/] AbsCC b_0'[//]H7) [*] (b_0'[/] b k[//]H10))).
apply un_op_wd_unfolded.
apply mult_wdl.
unfold cc_IR in |- *; simpl in |- *; split; simpl in |- *; rational.
Qed.
(* end hide *)
Expand Down

0 comments on commit af80963

Please sign in to comment.