no automatic Experiments/Everything.agda

agda · Jan 25, 2024 · c1f8592 · c1f8592
1 parent 0d253bd
commit c1f8592
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 28 deletions.
diff --git a/.gitignore b/.gitignore
@@ -6,4 +6,3 @@ Cubical/*/Everything.agda
 !Cubical/Core/Everything.agda
 !Cubical/Foundations/Everything.agda
 !Cubical/Codata/Everything.agda
-!Cubical/Experiments/Everything.agda
diff --git a/Cubical/Experiments/Everything.agda b/Cubical/Experiments/Everything.agda
diff --git a/Cubical/Experiments/HInt.agda b/Cubical/Experiments/HInt.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 {-
 
 Definition of the integers as a HIT inspired by slide 10 of (original

diff --git a/GNUmakefile b/GNUmakefile
@@ -35,11 +35,11 @@ check-everythings:
 
 .PHONY : gen-everythings
 gen-everythings:
-	$(EVERYTHINGS) gen-except Core Foundations Codata Experiments
+	$(EVERYTHINGS) gen-except Core Foundations Codata
 
 .PHONY : gen-and-check-everythings
 gen-and-check-everythings:
-	$(EVERYTHINGS) gen-except Core Foundations Codata Experiments
+	$(EVERYTHINGS) gen-except Core Foundations Codata
 	$(EVERYTHINGS) check Core Foundations Codata
 
 .PHONY : check-README