From 82fdb905721dc6b12fe83b9846210f4bbae8b99d Mon Sep 17 00:00:00 2001
From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com>
Date: Mon, 2 Sep 2024 09:02:17 +0200
Subject: [PATCH 1/3] Add link to Coq Platform Docs

---
 README.md | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/README.md b/README.md
index 6b08d8f0..17fe8e40 100644
--- a/README.md
+++ b/README.md
@@ -33,16 +33,16 @@ definitions are axiom-free.
 - [Installation](#installation)
 - [HoTT Variant](#hott-variant)
 
-## Live demo
-
-Try it now in your browser with [JSCoq](http://mattam82.github.io/Coq-Equations/assets/jsexamples/equations_intro.html)!
-
 ## Documentation
 
+- You can discover and learn Equations through [interactive tutorials](https://coq.inria.fr/platform-docs/) 
+  directly in your browser, or locally with Equations installed.
+
 - The [reference manual](http://github.com/mattam82/Coq-Equations/raw/main/doc/equations.pdf)
-  provides an introduction and a summary of the commands and options.
-  This introduction can also be followed interactively with Equations installed:
+  provides a summary of the commands and options, and a brief introduction.
+  This introduction can also be followed interactively with Equations installed,
   [equations_intro.v](http://github.com/mattam82/Coq-Equations/raw/main/doc/equations_intro.v)
+  or directly [lived](http://mattam82.github.io/Coq-Equations/assets/jsexamples/equations_intro.html).
 
 - A gallery of [examples](http://mattam82.github.io/Coq-Equations/examples) provides more consequent
   developments using Equations.
@@ -150,4 +150,4 @@ install `coq-hott` and then use:
 This will compile the `HoTT` library variant in addition to the standard one.
 Then, after `make install`, one can import the plugin in Coq, using:
 
-    From Equations Require Import HoTT.All.
\ No newline at end of file
+    From Equations Require Import HoTT.All.

From eb5cc98efba6156f6df70380e02d84d1b82d8c99 Mon Sep 17 00:00:00 2001
From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com>
Date: Mon, 2 Sep 2024 09:54:05 +0200
Subject: [PATCH 2/3] Update README.md

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 17fe8e40..405c3f57 100644
--- a/README.md
+++ b/README.md
@@ -42,7 +42,7 @@ definitions are axiom-free.
   provides a summary of the commands and options, and a brief introduction.
   This introduction can also be followed interactively with Equations installed,
   [equations_intro.v](http://github.com/mattam82/Coq-Equations/raw/main/doc/equations_intro.v)
-  or directly [lived](http://mattam82.github.io/Coq-Equations/assets/jsexamples/equations_intro.html).
+  or [interactively in your browser](http://mattam82.github.io/Coq-Equations/assets/jsexamples/equations_intro.html).
 
 - A gallery of [examples](http://mattam82.github.io/Coq-Equations/examples) provides more consequent
   developments using Equations.

From 56b667581e665880cf0bf08ac4d3bfe427ebcee1 Mon Sep 17 00:00:00 2001
From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com>
Date: Mon, 2 Sep 2024 10:34:27 +0200
Subject: [PATCH 3/3] Update README.md

---
 README.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 405c3f57..5380edbc 100644
--- a/README.md
+++ b/README.md
@@ -33,11 +33,13 @@ definitions are axiom-free.
 - [Installation](#installation)
 - [HoTT Variant](#hott-variant)
 
-## Documentation
+## Learning Equations
 
 - You can discover and learn Equations through [interactive tutorials](https://coq.inria.fr/platform-docs/) 
   directly in your browser, or locally with Equations installed.
 
+## Documentation
+
 - The [reference manual](http://github.com/mattam82/Coq-Equations/raw/main/doc/equations.pdf)
   provides a summary of the commands and options, and a brief introduction.
   This introduction can also be followed interactively with Equations installed,