Merge pull request #142 from andreykl/master

snippets changed: ch1 ch2 ch3 ch4 ch5 better reflect book content now

Author: gares

coq/Makefile

@@ -1,4 +1,4 @@
-files=ch0.v  ch1.v  ch2.v  ch3.v  ch4.v  ch6.v  ch7_1.v ch7_2.v ch7_3.v ch7_4.v ch7_5.v  ch8.v
+files=ch0.v  ch1.v  ch2.v  ch3.v  ch4.v ch5.v ch6.v  ch7_1.v ch7_2.v ch7_3.v ch7_4.v ch7_5.v  ch8.v
 
 all: check $(files:%.v=%.html) index.html node_modules
 

coq/README.md

@@ -1,14 +1,19 @@
 # The Mathematical Components book code listings for jsCoq.
 
-Code snippets are intended to be viewed using jsCoq (actual version is
-<a href="https://math-comp.github.io/snippets">here</a>), but you also can just
-open selected `.v` file in your favorite Galina code editor. To view pages in 
-your browser locally you need install `coq`, `mathcomp`, then do `npm install` 
-and `node app.js` to run node applicaion (app.js) and then open link 
-http://127.0.0.1:8010/ in your browser. A bit more detailed instructions are 
-provided below.
-
-You can view jscoq snippets <a href="https://math-comp.github.io/snippets">here</a>.
+You can view jscoq snippets <a href="https://math-comp.github.io/mcb/snippets/">here</a>
+just by open link in browser. Or it is possible to download and open usual .v file in
+your favorite Galina editor.
+
+Instructions below are given to view code snippets on localhost (mostly 
+for testing/developement purposes).
+
+Code snippets are intended to be viewed using jsCoq for usability (and can be found
+by the link above). To view pages in  your browser locally you need install `coq`, 
+`mathcomp`, then do `npm install` and `node app.js` to run node applicaion (app.js) 
+and then open link  http://127.0.0.1:8010/ in your browser. A bit more detailed 
+instructions are provided below.
+
+
 
 ## Installation & Run
 

coq/ch0.v

@@ -8,3 +8,8 @@ rewrite big_nat_recr //= IHn addnC -divnMDl //.
 by rewrite mulnS muln1 -addnA -mulSn -mulnS.
 Qed.
 
+(* Recommended headers *)
+(* From mathcomp Require Import all_ssreflect. *)
+(* Set Implicit Arguments. *)
+(* Unset Strict Implicit. *)
+(* Unset Printing Implicit Defensive. *)