coq-community · spitters · May 31, 2023 · May 31, 2023
diff --git a/algebra/CFields.v b/algebra/CFields.v
@@ -41,7 +41,6 @@
 (** printing [/]?[//] %\ensuremath{/?\ddagger}% #/?&Dagger;# *)
 
 Require Export CoRN.algebra.CRings.
-Set Automatic Introduction.
 
 Transparent sym_eq.
 Transparent f_equal.

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1,7 +1,6 @@
 
 Require Import Coq.Setoids.Setoid Coq.PArith.BinPos Coq.PArith.Pnat ZArith_base.
 
-Set Automatic Introduction.
 
 Section P_of_nat.
 
@@ -35,7 +34,7 @@
 apply lt_O_nat_of_P.
 Qed.

 #[global]
 Hint Immediate nat_of_P_nonzero.

 Lemma Plt_lt (p q: positive): Pos.lt p q <-> (nat_of_P p < nat_of_P q).

diff --git 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
@@ -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
@@ -8,8 +8,6 @@ Require Import
   CoRN.stdlib_omissions.Z
   CoRN.stdlib_omissions.Q.
 
-Set Automatic Introduction.
-Set Automatic Introduction.
 
 Open Scope Q_scope.