From 629fbc743f8b5e7623a6834f19885b2e379cb782 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 27 Feb 2018 17:02:31 +0100 Subject: Update headers following #6543. --- theories/Arith/Arith.v | 10 ++++++---- theories/Arith/Arith_base.v | 10 ++++++---- theories/Arith/Between.v | 10 ++++++---- theories/Arith/Bool_nat.v | 10 ++++++---- theories/Arith/Compare.v | 10 ++++++---- theories/Arith/Compare_dec.v | 10 ++++++---- theories/Arith/Div2.v | 10 ++++++---- theories/Arith/EqNat.v | 10 ++++++---- theories/Arith/Euclid.v | 10 ++++++---- theories/Arith/Even.v | 10 ++++++---- theories/Arith/Factorial.v | 10 ++++++---- theories/Arith/Gt.v | 10 ++++++---- theories/Arith/Le.v | 10 ++++++---- theories/Arith/Lt.v | 10 ++++++---- theories/Arith/Max.v | 10 ++++++---- theories/Arith/Min.v | 10 ++++++---- theories/Arith/Minus.v | 10 ++++++---- theories/Arith/Mult.v | 10 ++++++---- theories/Arith/PeanoNat.v | 10 ++++++---- theories/Arith/Peano_dec.v | 10 ++++++---- theories/Arith/Plus.v | 12 +++++++----- theories/Arith/Wf_nat.v | 10 ++++++---- theories/Bool/Bool.v | 10 ++++++---- theories/Bool/BoolEq.v | 10 ++++++---- theories/Bool/Bvector.v | 10 ++++++---- theories/Bool/DecBool.v | 10 ++++++---- theories/Bool/IfProp.v | 10 ++++++---- theories/Bool/Sumbool.v | 10 ++++++---- theories/Bool/Zerob.v | 10 ++++++---- theories/Classes/CEquivalence.v | 10 ++++++---- theories/Classes/CMorphisms.v | 10 ++++++---- theories/Classes/CRelationClasses.v | 10 ++++++---- theories/Classes/DecidableClass.v | 10 ++++++---- theories/Classes/EquivDec.v | 10 ++++++---- theories/Classes/Equivalence.v | 10 ++++++---- theories/Classes/Init.v | 10 ++++++---- theories/Classes/Morphisms.v | 10 ++++++---- theories/Classes/Morphisms_Prop.v | 10 ++++++---- theories/Classes/Morphisms_Relations.v | 10 ++++++---- theories/Classes/RelationClasses.v | 10 ++++++---- theories/Classes/RelationPairs.v | 16 +++++++++------- theories/Classes/SetoidClass.v | 10 ++++++---- theories/Classes/SetoidDec.v | 10 ++++++---- theories/Classes/SetoidTactics.v | 10 ++++++---- theories/Compat/AdmitAxiom.v | 10 ++++++---- theories/Compat/Coq85.v | 10 ++++++---- theories/Compat/Coq86.v | 10 ++++++---- theories/Compat/Coq87.v | 10 ++++++---- theories/FSets/FMapAVL.v | 16 +++++++++------- theories/FSets/FMapFacts.v | 16 +++++++++------- theories/FSets/FMapFullAVL.v | 16 +++++++++------- theories/FSets/FMapInterface.v | 16 +++++++++------- theories/FSets/FMapList.v | 16 +++++++++------- theories/FSets/FMapPositive.v | 16 +++++++++------- theories/FSets/FMapWeakList.v | 16 +++++++++------- theories/FSets/FMaps.v | 16 +++++++++------- theories/FSets/FSetAVL.v | 16 +++++++++------- theories/FSets/FSetBridge.v | 16 +++++++++------- theories/FSets/FSetCompat.v | 16 +++++++++------- theories/FSets/FSetDecide.v | 16 +++++++++------- theories/FSets/FSetEqProperties.v | 16 +++++++++------- theories/FSets/FSetFacts.v | 16 +++++++++------- theories/FSets/FSetInterface.v | 16 +++++++++------- theories/FSets/FSetList.v | 16 +++++++++------- theories/FSets/FSetPositive.v | 16 +++++++++------- theories/FSets/FSetProperties.v | 16 +++++++++------- theories/FSets/FSetToFiniteSet.v | 16 +++++++++------- theories/FSets/FSetWeakList.v | 16 +++++++++------- theories/FSets/FSets.v | 16 +++++++++------- theories/Init/Datatypes.v | 10 ++++++---- theories/Init/Decimal.v | 10 ++++++---- theories/Init/Logic.v | 10 ++++++---- theories/Init/Logic_Type.v | 10 ++++++---- theories/Init/Nat.v | 10 ++++++---- theories/Init/Notations.v | 10 ++++++---- theories/Init/Peano.v | 10 ++++++---- theories/Init/Prelude.v | 10 ++++++---- theories/Init/Specif.v | 10 ++++++---- theories/Init/Tactics.v | 10 ++++++---- theories/Init/Wf.v | 10 ++++++---- theories/Lists/List.v | 10 ++++++---- theories/Lists/ListDec.v | 10 ++++++---- theories/Lists/ListSet.v | 10 ++++++---- theories/Lists/ListTactics.v | 10 ++++++---- theories/Lists/SetoidList.v | 16 +++++++++------- theories/Lists/SetoidPermutation.v | 16 +++++++++------- theories/Lists/StreamMemo.v | 10 ++++++---- theories/Lists/Streams.v | 10 ++++++---- theories/Logic/Berardi.v | 10 ++++++---- theories/Logic/ChoiceFacts.v | 12 +++++++----- theories/Logic/Classical.v | 10 ++++++---- theories/Logic/ClassicalChoice.v | 10 ++++++---- theories/Logic/ClassicalDescription.v | 10 ++++++---- theories/Logic/ClassicalEpsilon.v | 12 +++++++----- theories/Logic/ClassicalFacts.v | 10 ++++++---- theories/Logic/ClassicalUniqueChoice.v | 10 ++++++---- theories/Logic/Classical_Pred_Type.v | 10 ++++++---- theories/Logic/Classical_Prop.v | 10 ++++++---- theories/Logic/ConstructiveEpsilon.v | 10 ++++++---- theories/Logic/Decidable.v | 10 ++++++---- theories/Logic/Description.v | 10 ++++++---- theories/Logic/Diaconescu.v | 10 ++++++---- theories/Logic/Epsilon.v | 10 ++++++---- theories/Logic/Eqdep.v | 10 ++++++---- theories/Logic/EqdepFacts.v | 10 ++++++---- theories/Logic/Eqdep_dec.v | 10 ++++++---- theories/Logic/ExtensionalFunctionRepresentative.v | 10 ++++++---- theories/Logic/ExtensionalityFacts.v | 10 ++++++---- theories/Logic/FinFun.v | 10 ++++++---- theories/Logic/FunctionalExtensionality.v | 10 ++++++---- theories/Logic/Hurkens.v | 10 ++++++---- theories/Logic/IndefiniteDescription.v | 10 ++++++---- theories/Logic/JMeq.v | 10 ++++++---- theories/Logic/ProofIrrelevance.v | 10 ++++++---- theories/Logic/ProofIrrelevanceFacts.v | 10 ++++++---- theories/Logic/PropExtensionality.v | 10 ++++++---- theories/Logic/PropExtensionalityFacts.v | 10 ++++++---- theories/Logic/PropFacts.v | 10 ++++++---- theories/Logic/RelationalChoice.v | 10 ++++++---- theories/Logic/SetIsType.v | 10 ++++++---- theories/Logic/SetoidChoice.v | 10 ++++++---- theories/Logic/WKL.v | 10 ++++++---- theories/Logic/WeakFan.v | 10 ++++++---- theories/MSets/MSetAVL.v | 16 +++++++++------- theories/MSets/MSetDecide.v | 16 +++++++++------- theories/MSets/MSetEqProperties.v | 16 +++++++++------- theories/MSets/MSetFacts.v | 16 +++++++++------- theories/MSets/MSetGenTree.v | 16 +++++++++------- theories/MSets/MSetInterface.v | 16 +++++++++------- theories/MSets/MSetList.v | 16 +++++++++------- theories/MSets/MSetPositive.v | 16 +++++++++------- theories/MSets/MSetProperties.v | 16 +++++++++------- theories/MSets/MSetRBT.v | 16 +++++++++------- theories/MSets/MSetToFiniteSet.v | 16 +++++++++------- theories/MSets/MSetWeakList.v | 16 +++++++++------- theories/MSets/MSets.v | 16 +++++++++------- theories/NArith/BinNat.v | 10 ++++++---- theories/NArith/BinNatDef.v | 10 ++++++---- theories/NArith/NArith.v | 10 ++++++---- theories/NArith/Ndec.v | 10 ++++++---- theories/NArith/Ndigits.v | 10 ++++++---- theories/NArith/Ndist.v | 10 ++++++---- theories/NArith/Ndiv_def.v | 10 ++++++---- theories/NArith/Ngcd_def.v | 10 ++++++---- theories/NArith/Nnat.v | 10 ++++++---- theories/NArith/Nsqrt_def.v | 10 ++++++---- theories/Numbers/BinNums.v | 10 ++++++---- theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 10 ++++++---- theories/Numbers/Cyclic/Abstract/DoubleType.v | 10 ++++++---- theories/Numbers/Cyclic/Abstract/NZCyclic.v | 10 ++++++---- theories/Numbers/Cyclic/Int31/Cyclic31.v | 10 ++++++---- theories/Numbers/Cyclic/Int31/Int31.v | 10 ++++++---- theories/Numbers/Cyclic/Int31/Ring31.v | 10 ++++++---- theories/Numbers/Cyclic/ZModulo/ZModulo.v | 10 ++++++---- theories/Numbers/DecimalFacts.v | 10 ++++++---- theories/Numbers/DecimalN.v | 10 ++++++---- theories/Numbers/DecimalNat.v | 10 ++++++---- theories/Numbers/DecimalPos.v | 10 ++++++---- theories/Numbers/DecimalString.v | 10 ++++++---- theories/Numbers/DecimalZ.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZAdd.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZAddOrder.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZAxioms.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZBase.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZBits.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZDivEucl.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZDivFloor.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZDivTrunc.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZGcd.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZLcm.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZLt.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZMaxMin.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZMul.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZMulOrder.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZParity.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZPow.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZProperties.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZSgnAbs.v | 10 ++++++---- theories/Numbers/Integer/Binary/ZBinary.v | 10 ++++++---- theories/Numbers/Integer/NatPairs/ZNatPairs.v | 10 ++++++---- theories/Numbers/NaryFunctions.v | 10 ++++++---- theories/Numbers/NatInt/NZAdd.v | 10 ++++++---- theories/Numbers/NatInt/NZAddOrder.v | 10 ++++++---- theories/Numbers/NatInt/NZAxioms.v | 10 ++++++---- theories/Numbers/NatInt/NZBase.v | 10 ++++++---- theories/Numbers/NatInt/NZBits.v | 10 ++++++---- theories/Numbers/NatInt/NZDiv.v | 10 ++++++---- theories/Numbers/NatInt/NZDomain.v | 10 ++++++---- theories/Numbers/NatInt/NZGcd.v | 10 ++++++---- theories/Numbers/NatInt/NZLog.v | 10 ++++++---- theories/Numbers/NatInt/NZMul.v | 10 ++++++---- theories/Numbers/NatInt/NZMulOrder.v | 10 ++++++---- theories/Numbers/NatInt/NZOrder.v | 10 ++++++---- theories/Numbers/NatInt/NZParity.v | 10 ++++++---- theories/Numbers/NatInt/NZPow.v | 10 ++++++---- theories/Numbers/NatInt/NZProperties.v | 10 ++++++---- theories/Numbers/NatInt/NZSqrt.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NAdd.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NAddOrder.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NAxioms.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NBase.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NBits.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NDefOps.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NDiv.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NGcd.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NIso.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NLcm.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NLog.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NMaxMin.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NMulOrder.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NOrder.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NParity.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NPow.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NProperties.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NSqrt.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NStrongRec.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NSub.v | 10 ++++++---- theories/Numbers/Natural/Binary/NBinary.v | 10 ++++++---- theories/Numbers/Natural/Peano/NPeano.v | 10 ++++++---- theories/Numbers/NumPrelude.v | 10 ++++++---- theories/PArith/BinPos.v | 10 ++++++---- theories/PArith/BinPosDef.v | 10 ++++++---- theories/PArith/PArith.v | 10 ++++++---- theories/PArith/POrderedType.v | 10 ++++++---- theories/PArith/Pnat.v | 10 ++++++---- theories/Program/Basics.v | 10 ++++++---- theories/Program/Combinators.v | 10 ++++++---- theories/Program/Equality.v | 10 ++++++---- theories/Program/Program.v | 10 ++++++---- theories/Program/Subset.v | 10 ++++++---- theories/Program/Syntax.v | 10 ++++++---- theories/Program/Tactics.v | 10 ++++++---- theories/Program/Utils.v | 10 ++++++---- theories/Program/Wf.v | 10 ++++++---- theories/QArith/QArith.v | 10 ++++++---- theories/QArith/QArith_base.v | 10 ++++++---- theories/QArith/QOrderedType.v | 10 ++++++---- theories/QArith/Qabs.v | 10 ++++++---- theories/QArith/Qcabs.v | 10 ++++++---- theories/QArith/Qcanon.v | 10 ++++++---- theories/QArith/Qfield.v | 10 ++++++---- theories/QArith/Qminmax.v | 10 ++++++---- theories/QArith/Qpower.v | 10 ++++++---- theories/QArith/Qreals.v | 10 ++++++---- theories/QArith/Qreduction.v | 10 ++++++---- theories/QArith/Qring.v | 10 ++++++---- theories/QArith/Qround.v | 10 ++++++---- theories/Reals/Alembert.v | 10 ++++++---- theories/Reals/AltSeries.v | 10 ++++++---- theories/Reals/ArithProp.v | 10 ++++++---- theories/Reals/Binomial.v | 10 ++++++---- theories/Reals/Cauchy_prod.v | 10 ++++++---- theories/Reals/Cos_plus.v | 10 ++++++---- theories/Reals/Cos_rel.v | 10 ++++++---- theories/Reals/DiscrR.v | 10 ++++++---- theories/Reals/Exp_prop.v | 10 ++++++---- theories/Reals/Integration.v | 10 ++++++---- theories/Reals/MVT.v | 10 ++++++---- theories/Reals/Machin.v | 10 ++++++---- theories/Reals/NewtonInt.v | 10 ++++++---- theories/Reals/PSeries_reg.v | 10 ++++++---- theories/Reals/PartSum.v | 10 ++++++---- theories/Reals/RIneq.v | 12 +++++++----- theories/Reals/RList.v | 10 ++++++---- theories/Reals/ROrderedType.v | 10 ++++++---- theories/Reals/R_Ifp.v | 10 ++++++---- theories/Reals/R_sqr.v | 10 ++++++---- theories/Reals/R_sqrt.v | 10 ++++++---- theories/Reals/Ranalysis.v | 10 ++++++---- theories/Reals/Ranalysis1.v | 10 ++++++---- theories/Reals/Ranalysis2.v | 10 ++++++---- theories/Reals/Ranalysis3.v | 10 ++++++---- theories/Reals/Ranalysis4.v | 10 ++++++---- theories/Reals/Ranalysis5.v | 10 ++++++---- theories/Reals/Ranalysis_reg.v | 10 ++++++---- theories/Reals/Ratan.v | 10 ++++++---- theories/Reals/Raxioms.v | 10 ++++++---- theories/Reals/Rbase.v | 10 ++++++---- theories/Reals/Rbasic_fun.v | 10 ++++++---- theories/Reals/Rcomplete.v | 10 ++++++---- theories/Reals/Rdefinitions.v | 10 ++++++---- theories/Reals/Rderiv.v | 10 ++++++---- theories/Reals/Reals.v | 10 ++++++---- theories/Reals/Rfunctions.v | 10 ++++++---- theories/Reals/Rgeom.v | 10 ++++++---- theories/Reals/RiemannInt.v | 10 ++++++---- theories/Reals/RiemannInt_SF.v | 10 ++++++---- theories/Reals/Rlimit.v | 10 ++++++---- theories/Reals/Rlogic.v | 10 ++++++---- theories/Reals/Rminmax.v | 10 ++++++---- theories/Reals/Rpow_def.v | 10 ++++++---- theories/Reals/Rpower.v | 10 ++++++---- theories/Reals/Rprod.v | 10 ++++++---- theories/Reals/Rseries.v | 10 ++++++---- theories/Reals/Rsigma.v | 10 ++++++---- theories/Reals/Rsqrt_def.v | 10 ++++++---- theories/Reals/Rtopology.v | 10 ++++++---- theories/Reals/Rtrigo.v | 10 ++++++---- theories/Reals/Rtrigo1.v | 10 ++++++---- theories/Reals/Rtrigo_alt.v | 10 ++++++---- theories/Reals/Rtrigo_calc.v | 10 ++++++---- theories/Reals/Rtrigo_def.v | 10 ++++++---- theories/Reals/Rtrigo_fun.v | 10 ++++++---- theories/Reals/Rtrigo_reg.v | 10 ++++++---- theories/Reals/SeqProp.v | 10 ++++++---- theories/Reals/SeqSeries.v | 10 ++++++---- theories/Reals/SplitAbsolu.v | 10 ++++++---- theories/Reals/SplitRmult.v | 10 ++++++---- theories/Reals/Sqrt_reg.v | 10 ++++++---- theories/Relations/Operators_Properties.v | 10 ++++++---- theories/Relations/Relation_Definitions.v | 10 ++++++---- theories/Relations/Relation_Operators.v | 10 ++++++---- theories/Relations/Relations.v | 10 ++++++---- theories/Setoids/Setoid.v | 10 ++++++---- theories/Sets/Classical_sets.v | 10 ++++++---- theories/Sets/Constructive_sets.v | 10 ++++++---- theories/Sets/Cpo.v | 10 ++++++---- theories/Sets/Ensembles.v | 10 ++++++---- theories/Sets/Finite_sets.v | 10 ++++++---- theories/Sets/Finite_sets_facts.v | 10 ++++++---- theories/Sets/Image.v | 10 ++++++---- theories/Sets/Infinite_sets.v | 10 ++++++---- theories/Sets/Integers.v | 10 ++++++---- theories/Sets/Multiset.v | 10 ++++++---- theories/Sets/Partial_Order.v | 10 ++++++---- theories/Sets/Permut.v | 10 ++++++---- theories/Sets/Powerset.v | 10 ++++++---- theories/Sets/Powerset_Classical_facts.v | 10 ++++++---- theories/Sets/Powerset_facts.v | 10 ++++++---- theories/Sets/Relations_1.v | 10 ++++++---- theories/Sets/Relations_1_facts.v | 10 ++++++---- theories/Sets/Relations_2.v | 10 ++++++---- theories/Sets/Relations_2_facts.v | 10 ++++++---- theories/Sets/Relations_3.v | 10 ++++++---- theories/Sets/Relations_3_facts.v | 10 ++++++---- theories/Sets/Uniset.v | 10 ++++++---- theories/Sorting/Heap.v | 10 ++++++---- theories/Sorting/Mergesort.v | 10 ++++++---- theories/Sorting/PermutEq.v | 10 ++++++---- theories/Sorting/PermutSetoid.v | 10 ++++++---- theories/Sorting/Permutation.v | 10 ++++++---- theories/Sorting/Sorted.v | 10 ++++++---- theories/Sorting/Sorting.v | 10 ++++++---- theories/Strings/Ascii.v | 12 +++++++----- theories/Strings/String.v | 10 ++++++---- theories/Structures/DecidableType.v | 16 +++++++++------- theories/Structures/DecidableTypeEx.v | 16 +++++++++------- theories/Structures/Equalities.v | 16 +++++++++------- theories/Structures/EqualitiesFacts.v | 16 +++++++++------- theories/Structures/GenericMinMax.v | 16 +++++++++------- theories/Structures/OrderedType.v | 16 +++++++++------- theories/Structures/OrderedTypeAlt.v | 16 +++++++++------- theories/Structures/OrderedTypeEx.v | 16 +++++++++------- theories/Structures/Orders.v | 16 +++++++++------- theories/Structures/OrdersAlt.v | 16 +++++++++------- theories/Structures/OrdersEx.v | 16 +++++++++------- theories/Structures/OrdersFacts.v | 16 +++++++++------- theories/Structures/OrdersLists.v | 16 +++++++++------- theories/Structures/OrdersTac.v | 16 +++++++++------- theories/Unicode/Utf8.v | 10 ++++++---- theories/Unicode/Utf8_core.v | 10 ++++++---- theories/Vectors/Fin.v | 10 ++++++---- theories/Vectors/Vector.v | 10 ++++++---- theories/Vectors/VectorDef.v | 10 ++++++---- theories/Vectors/VectorEq.v | 10 ++++++---- theories/Vectors/VectorSpec.v | 10 ++++++---- theories/Wellfounded/Disjoint_Union.v | 10 ++++++---- theories/Wellfounded/Inclusion.v | 10 ++++++---- theories/Wellfounded/Inverse_Image.v | 10 ++++++---- theories/Wellfounded/Lexicographic_Exponentiation.v | 10 ++++++---- theories/Wellfounded/Lexicographic_Product.v | 10 ++++++---- theories/Wellfounded/Transitive_Closure.v | 10 ++++++---- theories/Wellfounded/Union.v | 10 ++++++---- theories/Wellfounded/Well_Ordering.v | 10 ++++++---- theories/Wellfounded/Wellfounded.v | 10 ++++++---- theories/ZArith/BinInt.v | 10 ++++++---- theories/ZArith/BinIntDef.v | 10 ++++++---- theories/ZArith/Int.v | 16 +++++++++------- theories/ZArith/Wf_Z.v | 10 ++++++---- theories/ZArith/ZArith.v | 10 ++++++---- theories/ZArith/ZArith_base.v | 10 ++++++---- theories/ZArith/ZArith_dec.v | 10 ++++++---- theories/ZArith/Zabs.v | 10 ++++++---- theories/ZArith/Zbool.v | 10 ++++++---- theories/ZArith/Zcompare.v | 10 ++++++---- theories/ZArith/Zcomplements.v | 10 ++++++---- theories/ZArith/Zdigits.v | 10 ++++++---- theories/ZArith/Zdiv.v | 10 ++++++---- theories/ZArith/Zeuclid.v | 10 ++++++---- theories/ZArith/Zeven.v | 10 ++++++---- theories/ZArith/Zgcd_alt.v | 10 ++++++---- theories/ZArith/Zhints.v | 10 ++++++---- theories/ZArith/Zlogarithm.v | 10 ++++++---- theories/ZArith/Zmax.v | 10 ++++++---- theories/ZArith/Zmin.v | 10 ++++++---- theories/ZArith/Zminmax.v | 10 ++++++---- theories/ZArith/Zmisc.v | 10 ++++++---- theories/ZArith/Znat.v | 10 ++++++---- theories/ZArith/Znumtheory.v | 10 ++++++---- theories/ZArith/Zorder.v | 10 ++++++---- theories/ZArith/Zpow_alt.v | 10 ++++++---- theories/ZArith/Zpow_def.v | 10 ++++++---- theories/ZArith/Zpow_facts.v | 10 ++++++---- theories/ZArith/Zpower.v | 10 ++++++---- theories/ZArith/Zquot.v | 10 ++++++---- theories/ZArith/Zsqrt_compat.v | 10 ++++++---- theories/ZArith/Zwf.v | 10 ++++++---- theories/ZArith/auxiliary.v | 10 ++++++---- 408 files changed, 2609 insertions(+), 1793 deletions(-) (limited to 'theories') diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 649819878..1cba8fafe 100644 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 04062fbbd..d6b386f10 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*