Changed import.

klinashka · klinashka · commit 8cfcc806c7f4 · 2024-11-14T16:22:20.000+01:00
diff --git a/code/Decidability/DiscreteTypes.v b/code/Decidability/DiscreteTypes.v
@@ -1,4 +1,4 @@
-Require Export UniMath.Foundations.All.
+Require Import init.imports.
   
 Section EqualityDeciders.
 
diff --git a/code/_CoqProject b/code/_CoqProject
@@ -5,8 +5,7 @@ COQDEP = coqdep
 -arg "-w -notation-overridden -type-in-type"
 
 init/imports.v
+init/all.v
 
 Decidability/DecidablePredicates.v
-Decidability/DiscreteTypes.v
-
-
+Decidability/DiscreteTypes.v
diff --git a/code/init/all.v b/code/init/all.v
@@ -0,0 +1,3 @@
+
+
+Require Export init.imports.

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-Require Export UniMath.Foundations.All.`
	`1`	`+Require Import init.imports.`
`2`	`2`
`3`	`3`	`Section EqualityDeciders.`
`4`	`4`