Use primitive projections, use qualified imports

artagnon · Feb 6, 2024 · f5f42f9 · f5f42f9
1 parent ac3d456
commit f5f42f9
Show file tree

Hide file tree

Showing 6 changed files with 27 additions and 11 deletions.
diff --git 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/νType/HSet.v b/theories/νType/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/νType/LeInductive.v b/theories/νType/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/νType/LeYoneda.v b/theories/νType/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/νType/RewLemmas.v b/theories/νType/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/νType/νType.v b/theories/νType/νType.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.