diff --git a/.vscode/settings.json b/.vscode/settings.json
index 479ff95..520f16c 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -5,5 +5,19 @@
   ],
   "spellright.documentTypes": [
     "latex",
-  ]
+  ],
+  "files.exclude": {
+    "**/*.vo": true,
+    "**/*.vok": true,
+    "**/*.vos": true,
+    "**/*.aux": true,
+    "**/*.glob": true,
+    "**/.git": true,
+    "**/.svn": false,
+    "**/.hg": false,
+    "**/CVS": false,
+    "**/.DS_Store": true,
+    "**/Thumbs.db": true,
+    "**/.ruby-lsp": true
+  }
 }
diff --git "a/theories/\316\275Type/HSet.v" "b/theories/\316\275Type/HSet.v"
index cd3b0af..feaea22 100644
--- "a/theories/\316\275Type/HSet.v"
+++ "b/theories/\316\275Type/HSet.v"
@@ -2,8 +2,9 @@
 
 Require Import Logic.FunctionalExtensionality.
 Require Import Logic.Eqdep_dec. (* UIP_refl_unit *)
-Require Import Notation.
+From Bonak Require Import Notation.
 
+Set Primitive Projections.
 Set Universe Polymorphism.
 
 Record HSet := {
diff --git "a/theories/\316\275Type/LeInductive.v" "b/theories/\316\275Type/LeInductive.v"
index d73e566..e0efd66 100644
--- "a/theories/\316\275Type/LeInductive.v"
+++ "b/theories/\316\275Type/LeInductive.v"
@@ -1,4 +1,4 @@
-Require Import Notation.
+From Bonak Require Import Notation.
 
 (** An inductive definition of le *)
 Reserved Infix "<~" (at level 70).
diff --git "a/theories/\316\275Type/LeYoneda.v" "b/theories/\316\275Type/LeYoneda.v"
index 18f110d..a543e2d 100644
--- "a/theories/\316\275Type/LeYoneda.v"
+++ "b/theories/\316\275Type/LeYoneda.v"
@@ -2,8 +2,8 @@
     - Recursive definition
     - "Yoneda trick" *)
 
-Require Import Notation.
-Require Import LeInductive.
+From Bonak Require Import Notation.
+From Bonak Require Import LeInductive.
 
 Set Warnings "-notation-overridden".
 
diff --git "a/theories/\316\275Type/RewLemmas.v" "b/theories/\316\275Type/RewLemmas.v"
index 69da76c..2fb5cb8 100644
--- "a/theories/\316\275Type/RewLemmas.v"
+++ "b/theories/\316\275Type/RewLemmas.v"
@@ -1,7 +1,7 @@
 (** A few rewriting lemmas not in the standard library *)
 
 Import Logic.EqNotations.
-Require Import Notation.
+From Bonak Require Import Notation.
 
 Lemma rew_rew {A} {x y: A} (H : x = y) P {a: P x} :
 rew <- [P] H in rew [P] H in a = a.
diff --git "a/theories/\316\275Type/\316\275Type.v" "b/theories/\316\275Type/\316\275Type.v"
index 74b79d2..14d57f1 100644
--- "a/theories/\316\275Type/\316\275Type.v"
+++ "b/theories/\316\275Type/\316\275Type.v"
@@ -4,15 +4,16 @@
 
 Import Logic.EqNotations.
 Require Import Logic.FunctionalExtensionality.
-Require Import Notation.
-Require Import RewLemmas.
+From Bonak Require Import Notation.
+From Bonak Require Import RewLemmas.
 
 (* Note: this import overrides { & } notation and introduces hforall *)
 Set Warnings "-notation-overridden".
-Require Import HSet.
+From Bonak Require Import HSet.
 
-Require Import LeYoneda.
+From Bonak Require Import LeYoneda.
 
+Set Primitive Projections.
 Set Printing Projections.
 Set Keyed Unification.
 Remove Printing Let sigT.
@@ -525,7 +526,7 @@ Proof.
   simpl (mkFrame p.+1). unfold mkPaintingPrev, painting''.
   change (fun x => C.(PaintingPrev).(painting') (Hp := ?Hp) (D := ?D) x) with
     (C.(PaintingPrev).(painting') (Hp := Hp) (D := D)).
-  unfold mkFrameSp; unfold cohFrame at -1.
+  unfold mkFrameSp, cohFrame.
   rewrite rew_map with (P := fun x => (C.(PaintingPrev).(painting') x).(Dom))
                        (f := fun x => rew <- [id] C.(eqFrameSp') in x).
   repeat rewrite rew_compose.