diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml
new file mode 100644
index 0000000000..f1b4f7bf01
--- /dev/null
+++ b/.github/workflows/deploy.yml
@@ -0,0 +1,89 @@
+name: Deploy
+on:
+  push:
+    branches:
+      - master
+
+jobs:
+  build-guide:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+      - name: Install latest mdbook
+        run: |
+          tag=$(curl 'https://api.github.com/repos/rust-lang/mdbook/releases/latest' | jq -r '.tag_name')
+          url="https://github.com/rust-lang/mdbook/releases/download/${tag}/mdbook-${tag}-x86_64-unknown-linux-gnu.tar.gz"
+          mkdir mdbook
+          curl -sSL $url | tar -xz --directory=./mdbook
+          echo `pwd`/mdbook >> $GITHUB_PATH
+      - name: Build Book
+        run: |
+          mdbook build guide
+      - name: Upload guide artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: guide
+          path: |
+            guide/book/
+  
+  build-docs:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+    - uses: actions/cache@v4
+      with:
+        path: |
+          ~/.rustup
+          ~/.cargo/registry
+          ~/.cargo/git
+          target
+        key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+    - name: Build creusot-rustc
+      run: cargo build -p creusot-rustc --release
+    - name: Dummy creusot setup
+      run: |
+        mkdir -p ~/.config/creusot
+        cp ci/creusot-config-dummy.toml ~/.config/creusot/Config.toml
+    - name: Build doc
+      run: cargo run -p cargo-creusot --release -- creusot doc -- -p creusot-contracts --no-deps
+    - name: Upload creusot_contracts artifact
+      uses: actions/upload-artifact@v4
+      with:
+        name: creusot_contracts
+        path: |
+          target/doc/
+  
+  deploy:
+    needs: [build-guide, build-docs]
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write  # To push a branch 
+      pages: write  # To push to a GitHub Pages site
+      id-token: write # To update the deployment status
+    steps:
+    - name: Remove previous dir
+      run: |
+        rm -rf ci/deploy-output
+    - name: Download guide artifact
+      uses: actions/download-artifact@v4
+      with:
+        name: guide
+        path: ci/deploy-output/guide/
+    - name: Download creusot_contracts artifact
+      uses: actions/download-artifact@v4
+      with:
+        name: creusot_contracts
+        path: ci/deploy-output/doc/
+    - name: Setup Pages
+      uses: actions/configure-pages@v2
+    - name: Upload artifact
+      uses: actions/upload-pages-artifact@v1
+      with:
+        path: 'ci/deploy-output'
+    - name: Deploy to GitHub Pages
+      id: deployment
+      uses: actions/deploy-pages@v1
\ No newline at end of file
diff --git a/.github/workflows/guide.yml b/.github/workflows/guide.yml
deleted file mode 100644
index 1ef0589a19..0000000000
--- a/.github/workflows/guide.yml
+++ /dev/null
@@ -1,37 +0,0 @@
-name: Deploy
-on:
-  push:
-    branches:
-      - master
-
-jobs:
-  deploy:
-    runs-on: ubuntu-latest
-    permissions:
-      contents: write  # To push a branch 
-      pages: write  # To push to a GitHub Pages site
-      id-token: write # To update the deployment status
-    steps:
-      - uses: actions/checkout@v3
-        with:
-          fetch-depth: 0
-      - name: Install latest mdbook
-        run: |
-          tag=$(curl 'https://api.github.com/repos/rust-lang/mdbook/releases/latest' | jq -r '.tag_name')
-          url="https://github.com/rust-lang/mdbook/releases/download/${tag}/mdbook-${tag}-x86_64-unknown-linux-gnu.tar.gz"
-          mkdir mdbook
-          curl -sSL $url | tar -xz --directory=./mdbook
-          echo `pwd`/mdbook >> $GITHUB_PATH
-      - name: Build Book
-        run: |
-          mdbook build guide
-      - name: Setup Pages
-        uses: actions/configure-pages@v2
-      - name: Upload artifact
-        uses: actions/upload-pages-artifact@v1
-        with:
-          # Upload entire repository
-          path: 'guide/book'
-      - name: Deploy to GitHub Pages
-        id: deployment
-        uses: actions/deploy-pages@v1
\ No newline at end of file
diff --git a/README.md b/README.md
index 2e0d823842..1576ea2455 100644
--- a/README.md
+++ b/README.md
@@ -88,8 +88,8 @@ More examples are found in [creusot/tests/should_succeed](creusot/tests/should_s
 
 # Verifying with Creusot and Why3
 
-See the [guide](https://creusot-rs.github.io/creusot/).
-
+- To learn how to write code with creusot: [guide](https://creusot-rs.github.io/creusot/guide)
+- To see the API of `creusot_contracts` (creusot's "standart library"): [creusot_contracts API](https://creusot-rs.github.io/creusot/doc/creusot_contracts)
 
 # Hacking on Creusot
 
diff --git a/creusot-contracts/src/lib.rs b/creusot-contracts/src/lib.rs
index 07e9bea5d5..c6f0519fa8 100644
--- a/creusot-contracts/src/lib.rs
+++ b/creusot-contracts/src/lib.rs
@@ -178,6 +178,7 @@ mod macros {
     pub use base_macros::open_inv_result;
 }
 
+#[doc(hidden)]
 #[cfg(creusot)]
 #[path = "stubs.rs"]
 pub mod __stubs;
diff --git a/creusot/tests/should_succeed/syntax/13_vec_macro.coma b/creusot/tests/should_succeed/syntax/13_vec_macro.coma
index 7ada89680b..718be3b03a 100644
--- a/creusot/tests/should_succeed/syntax/13_vec_macro.coma
+++ b/creusot/tests/should_succeed/syntax/13_vec_macro.coma
@@ -1,5 +1,5 @@
 module M_13_vec_macro__x [#"13_vec_macro.rs" 5 0 5 10]
-  let%span slib0 = "../../../../creusot-contracts/src/lib.rs" 270 8 270 30
+  let%span slib0 = "../../../../creusot-contracts/src/lib.rs" 271 8 271 30
   let%span s13_vec_macro1 = "13_vec_macro.rs" 7 20 7 34
   let%span s13_vec_macro2 = "13_vec_macro.rs" 9 18 9 19
   let%span s13_vec_macro3 = "13_vec_macro.rs" 9 21 9 22