diff --git a/algebra/CFields.v b/algebra/CFields.v
index 139641cd..83a13e0a 100644
--- a/algebra/CFields.v
+++ b/algebra/CFields.v
@@ -41,7 +41,6 @@
 (** printing [/]?[//] %\ensuremath{/?\ddagger}% #/?‡# *)
 
 Require Export CoRN.algebra.CRings.
-Set Automatic Introduction.
 
 Transparent sym_eq.
 Transparent f_equal.
diff --git a/algebra/CGroups.v b/algebra/CGroups.v
index e44798da..8b0d6336 100644
--- a/algebra/CGroups.v
+++ b/algebra/CGroups.v
@@ -42,7 +42,6 @@
 
 Require Import CoRN.tactics.CornTac.
 Require Export CoRN.algebra.CMonoids.
-Set Automatic Introduction.
 
 (* Begin_SpecReals *)
 
diff --git a/algebra/COrdCauchy.v b/algebra/COrdCauchy.v
index 0dd60198..726c3b6b 100644
--- a/algebra/COrdCauchy.v
+++ b/algebra/COrdCauchy.v
@@ -35,7 +35,6 @@
  *)
 Require Export CoRN.algebra.COrdAbs.
 From Coq Require Import Lia.
-Set Automatic Introduction.
 
 (* Begin_SpecReals *)
 
diff --git a/algebra/CPoly_ApZero.v b/algebra/CPoly_ApZero.v
index 66150ded..e250d1d5 100644
--- a/algebra/CPoly_ApZero.v
+++ b/algebra/CPoly_ApZero.v
@@ -41,7 +41,6 @@ Require MathClasses.implementations.ne_list.
 Import CRing_Homomorphisms.coercions.
 Import ne_list.notations ne_list.coercions.
 
-Set Automatic Introduction.
 
 (**
 * Polynomials apart from zero *)
diff --git a/algebra/CPoly_Degree.v b/algebra/CPoly_Degree.v
index c8febc62..74e088c3 100644
--- a/algebra/CPoly_Degree.v
+++ b/algebra/CPoly_Degree.v
@@ -39,7 +39,6 @@ Require Export CoRN.algebra.CFields.
 Require Export CoRN.tactics.Rational.
 Require Import Lia.
 Import CRing_Homomorphisms.coercions.
-Set Automatic Introduction.
 
 (**
 * Degrees of Polynomials
diff --git a/algebra/CPoly_Newton.v b/algebra/CPoly_Newton.v
index df74a476..e0866629 100644
--- a/algebra/CPoly_Newton.v
+++ b/algebra/CPoly_Newton.v
@@ -10,7 +10,6 @@ Require MathClasses.implementations.ne_list.
 Import CRing_Homomorphisms.coercions.
 Import ne_list.notations ne_list.coercions.
 
-Set Automatic Introduction.
 
 Coercion Vector.to_list: Vector.t >-> list.
 
diff --git a/algebra/CRing_Homomorphisms.v b/algebra/CRing_Homomorphisms.v
index 20e7aed1..b4a0ba99 100644
--- a/algebra/CRing_Homomorphisms.v
+++ b/algebra/CRing_Homomorphisms.v
@@ -47,7 +47,6 @@
 (** printing phi %\ensuremath{\phi}%  *)
 
 Require Export CoRN.algebra.CRings.
-Set Automatic Introduction.
 
 (* Backwards compatibility for Hint Rewrite locality attributes *)
 Set Warnings "-unsupported-attributes".
diff --git a/ftc/FunctSums.v b/ftc/FunctSums.v
index 6062fdf4..bc9168e1 100644
--- a/ftc/FunctSums.v
+++ b/ftc/FunctSums.v
@@ -40,7 +40,6 @@
 
 Require Export CoRN.reals.CSumsReals.
 Require Export CoRN.ftc.PartFunEquality.
-Set Automatic Introduction.
 
 (**
 * Sums of Functions
diff --git a/ftc/NthDerivative.v b/ftc/NthDerivative.v
index 57bf3e25..1b63277b 100644
--- a/ftc/NthDerivative.v
+++ b/ftc/NthDerivative.v
@@ -35,7 +35,6 @@
  *)
 
 Require Export CoRN.ftc.Differentiability.
-Set Automatic Introduction.
 
 Section Nth_Derivative.
 
diff --git a/logic/CLogic.v b/logic/CLogic.v
index 4bd6922e..c0d41d99 100644
--- a/logic/CLogic.v
+++ b/logic/CLogic.v
@@ -52,7 +52,6 @@ Require Export Coq.Arith.Div2.
 Require Export Coq.Arith.Wf_nat.
 From Coq Require Import Lia.
 
-Set Automatic Introduction.
 
 (**
 * Extending the Coq Logic
diff --git a/logic/CornBasics.v b/logic/CornBasics.v
index f52ac509..73c248bc 100644
--- a/logic/CornBasics.v
+++ b/logic/CornBasics.v
@@ -71,9 +71,7 @@ Tactic Notation "apply" ":" constr(x) := pose proof x as HHH; first [
   refine (HHH _ _ _ _ _ _ _ _ _ _ _ _ _) |
   refine (HHH _ _ _ _ _ _ _ _ _ _ _ _ _ _)]; clear HHH.
 
-Global Set Automatic Coercions Import.
 
-Global Set Automatic Introduction.
 
 #[global]
 Instance: @DefaultRelation nat eq | 2 := {}.
diff --git a/metric2/Compact.v b/metric2/Compact.v
index 101f21d4..9684722b 100644
--- a/metric2/Compact.v
+++ b/metric2/Compact.v
@@ -29,7 +29,6 @@ Require Import Coq.QArith.Qround.
 Require Import Coq.Arith.Div2.
 
 Set Implicit Arguments.
-Set Automatic Introduction.
 
 Local Open Scope uc_scope.
 
diff --git a/metric2/Prelength.v b/metric2/Prelength.v
index c0899578..0d3b03fa 100644
--- a/metric2/Prelength.v
+++ b/metric2/Prelength.v
@@ -29,7 +29,6 @@ Require Import CoRN.stdlib_omissions.Q.
 
 
 Set Implicit Arguments.
-Set Automatic Introduction.
 
 Local Open Scope Q_scope.
 
diff --git a/metric2/StepFunctionSetoid.v b/metric2/StepFunctionSetoid.v
index df8255f2..686399a8 100644
--- a/metric2/StepFunctionSetoid.v
+++ b/metric2/StepFunctionSetoid.v
@@ -30,7 +30,6 @@ Require Import CoRN.algebra.COrdFields.
 Set Warnings "-unsupported-attributes".
 
 Set Implicit Arguments.
-Set Automatic Introduction.
 
 Local Open Scope Q_scope.
 
diff --git a/metrics/CMetricSpaces.v b/metrics/CMetricSpaces.v
index 2b75e4de..12d64f5f 100644
--- a/metrics/CMetricSpaces.v
+++ b/metrics/CMetricSpaces.v
@@ -36,7 +36,6 @@
 
 Require Export CoRN.metrics.Prod_Sub.
 Require Export CoRN.metrics.Equiv.
-Set Automatic Introduction.
 
 Section Definition_MS.
 (**
diff --git a/metrics/Prod_Sub.v b/metrics/Prod_Sub.v
index 438d44af..47c5e087 100644
--- a/metrics/Prod_Sub.v
+++ b/metrics/Prod_Sub.v
@@ -35,7 +35,6 @@
  *)
 
 Require Export CoRN.metrics.IR_CPMSpace.
-Set Automatic Introduction.
 
 Section prodpsmetrics.
 (**
diff --git a/model/metric2/LinfMetricMonad.v b/model/metric2/LinfMetricMonad.v
index 27e6281b..01b27009 100644
--- a/model/metric2/LinfMetricMonad.v
+++ b/model/metric2/LinfMetricMonad.v
@@ -39,7 +39,6 @@ Require Import CoRN.algebra.COrdFields2.
 Require Import CoRN.tactics.CornTac.
 
 Set Implicit Arguments.
-Set Automatic Introduction.
 
 Local Open Scope sfstscope.
 Local Open Scope setoid_scope.
diff --git a/model/metric2/Qmetric.v b/model/metric2/Qmetric.v
index 5ea377ab..61c5ed5e 100644
--- a/model/metric2/Qmetric.v
+++ b/model/metric2/Qmetric.v
@@ -29,7 +29,6 @@ Require Import CoRN.metric2.UniformContinuity.
 Require Import MathClasses.implementations.stdlib_rationals.
 
 Set Implicit Arguments.
-Set Automatic Introduction.
 
 Local Open Scope Q_scope.
 
diff --git a/model/setoids/Nfinsetoid.v b/model/setoids/Nfinsetoid.v
index a9164a09..dc864f2d 100644
--- a/model/setoids/Nfinsetoid.v
+++ b/model/setoids/Nfinsetoid.v
@@ -35,7 +35,6 @@
  *)
 
 Require Import CoRN.algebra.CSetoids.
-Set Automatic Introduction.
 
 (**
 ** Setoids of the first [n] natural numbers
diff --git a/model/setoids/Nsetoid.v b/model/setoids/Nsetoid.v
index b51c1e5e..b78bdbda 100644
--- a/model/setoids/Nsetoid.v
+++ b/model/setoids/Nsetoid.v
@@ -37,7 +37,6 @@
 Require Export CoRN.model.structures.Nsec.
 Require Import CoRN.algebra.CSetoidFun.
 
-Set Automatic Introduction.
 
 (**
 ** Example of a setoid: [nat]
diff --git a/model/setoids/Zfinsetoid.v b/model/setoids/Zfinsetoid.v
index 66034b63..344985b6 100644
--- a/model/setoids/Zfinsetoid.v
+++ b/model/setoids/Zfinsetoid.v
@@ -35,7 +35,6 @@
  *)
 Require Export Coq.ZArith.ZArith.
 Require Import CoRN.algebra.CSetoids.
-Set Automatic Introduction.
 
 (**
 ** Setoids of the integers between 0 and [z]
diff --git a/model/setoids/decsetoid.v b/model/setoids/decsetoid.v
index 75e527ca..96cd858f 100644
--- a/model/setoids/decsetoid.v
+++ b/model/setoids/decsetoid.v
@@ -10,7 +10,6 @@ Require Import
  Coq.Classes.Morphisms
  Coq.Classes.SetoidClass.
 
-Set Automatic Introduction.
 
 Class Apartness `{SetoidClass.Setoid} (ap: Crelation A): Type :=
   { ap_irreflexive: irreflexive ap
diff --git a/model/structures/QnonNeg.v b/model/structures/QnonNeg.v
index 979ca728..f9471a15 100644
--- a/model/structures/QnonNeg.v
+++ b/model/structures/QnonNeg.v
@@ -3,7 +3,6 @@
 Require Import CoRN.model.totalorder.QposMinMax 
         Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax.
 
-Set Automatic Introduction.
 
 (* The data type and simple relations/constants: *)
 
diff --git a/model/totalorder/QMinMax.v b/model/totalorder/QMinMax.v
index 55493bf2..bb3b2df4 100644
--- a/model/totalorder/QMinMax.v
+++ b/model/totalorder/QMinMax.v
@@ -21,7 +21,6 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 
 Require Import Coq.QArith.QArith_base.
 Require Import CoRN.order.TotalOrder.
-Set Automatic Introduction.
 
 (**
 ** Example of a Total Order: <Q, Qle, Qmin, Qmax>
diff --git a/reals/Intervals.v b/reals/Intervals.v
index 6362a9d6..4bd37a6b 100644
--- a/reals/Intervals.v
+++ b/reals/Intervals.v
@@ -36,7 +36,6 @@
 
 Require Export CoRN.algebra.CSetoidInc.
 Require Export CoRN.reals.RealLists.
-Set Automatic Introduction.
 
 Section Intervals.
 
diff --git a/reals/RealCount.v b/reals/RealCount.v
index 08105fe7..f7a137af 100644
--- a/reals/RealCount.v
+++ b/reals/RealCount.v
@@ -34,7 +34,6 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 Require Export CoRN.reals.CReals1.
-Set Automatic Introduction.
 
 (* Consider Reals are enumerated by function f *)
 
diff --git a/reals/fast/CRGroupOps.v b/reals/fast/CRGroupOps.v
index 5608e2fa..4e24c9fa 100644
--- a/reals/fast/CRGroupOps.v
+++ b/reals/fast/CRGroupOps.v
@@ -34,7 +34,6 @@ Require Import MathClasses.interfaces.canonical_names.
 Set Warnings "-unsupported-attributes".
 
 Set Implicit Arguments.
-Set Automatic Introduction.
 
 Opaque CR Qmin Qmax.
 
diff --git a/reals/fast/CRcorrect.v b/reals/fast/CRcorrect.v
index 661edbe5..2e5bab7c 100644
--- a/reals/fast/CRcorrect.v
+++ b/reals/fast/CRcorrect.v
@@ -34,7 +34,6 @@ Require Export CoRN.reals.fast.CRFieldOps.
 (* Backwards compatibility for Hint Rewrite locality attributes *)
 Set Warnings "-unsupported-attributes".
 
-Set Automatic Introduction.
 
 Local Open Scope nat_scope.
 
diff --git a/stdlib_omissions/P.v b/stdlib_omissions/P.v
index f0ccf265..b0191c20 100644
--- a/stdlib_omissions/P.v
+++ b/stdlib_omissions/P.v
@@ -1,7 +1,6 @@
 
 Require Import Coq.Setoids.Setoid Coq.PArith.BinPos Coq.PArith.Pnat ZArith_base.
 
-Set Automatic Introduction.
 
 Section P_of_nat.
 
diff --git a/stdlib_omissions/Q.v b/stdlib_omissions/Q.v
index ed103d00..2e645247 100644
--- a/stdlib_omissions/Q.v
+++ b/stdlib_omissions/Q.v
@@ -5,7 +5,6 @@ Require Import
 
 Require CoRN.stdlib_omissions.Z.
 
-Set Automatic Introduction.
 
 Notation "x <= y < z" := (x <= y /\ y < z) : Q_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : Q_scope.
diff --git a/util/Qgcd.v b/util/Qgcd.v
index 44daf800..2d0c4967 100644
--- a/util/Qgcd.v
+++ b/util/Qgcd.v
@@ -3,7 +3,6 @@ Require Import
         Coq.QArith.QArith CoRN.model.Zmod.ZGcd
         CoRN.model.totalorder.QposMinMax
         CoRN.stdlib_omissions.Q.
-Set Automatic Introduction.
 
 Open Scope Q_scope.
 
diff --git a/util/Qsums.v b/util/Qsums.v
index 06358cf7..eeb5ea71 100644
--- a/util/Qsums.v
+++ b/util/Qsums.v
@@ -8,8 +8,6 @@ Require Import
   CoRN.stdlib_omissions.Z
   CoRN.stdlib_omissions.Q.
 
-Set Automatic Introduction.
-Set Automatic Introduction.
 
 Open Scope Q_scope.