diff options
author | Matej Kosik <matej.kosik@inria.fr> | 2017-03-23 12:56:24 +0100 |
---|---|---|
committer | Matej Kosik <matej.kosik@inria.fr> | 2017-06-01 17:33:19 +0200 |
commit | 718d61a54157733bca61ed84c0ba3761cd52720f (patch) | |
tree | 4c57fa4ad6d75c5fc4f5747289dfed82d83dfc9a /theories | |
parent | 7fff12d45c4d86fa5cb9be3883084ffef5911405 (diff) |
drop vo.itarget files and compute the corresponding the corresponding values automatically instead
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Arith/vo.itarget | 22 | ||||
-rw-r--r-- | theories/Bool/vo.itarget | 7 | ||||
-rw-r--r-- | theories/Classes/vo.itarget | 15 | ||||
-rw-r--r-- | theories/Compat/vo.itarget | 4 | ||||
-rw-r--r-- | theories/FSets/vo.itarget | 21 | ||||
-rw-r--r-- | theories/Init/vo.itarget | 11 | ||||
-rw-r--r-- | theories/Lists/vo.itarget | 8 | ||||
-rw-r--r-- | theories/MSets/vo.itarget | 13 | ||||
-rw-r--r-- | theories/NArith/vo.itarget | 10 | ||||
-rw-r--r-- | theories/Numbers/vo.itarget | 91 | ||||
-rw-r--r-- | theories/PArith/vo.itarget | 5 | ||||
-rw-r--r-- | theories/Program/vo.itarget | 9 | ||||
-rw-r--r-- | theories/QArith/vo.itarget | 13 | ||||
-rw-r--r-- | theories/Reals/vo.itarget | 62 | ||||
-rw-r--r-- | theories/Relations/vo.itarget | 4 | ||||
-rw-r--r-- | theories/Setoids/vo.itarget | 1 | ||||
-rw-r--r-- | theories/Sets/vo.itarget | 22 | ||||
-rw-r--r-- | theories/Sorting/vo.itarget | 7 | ||||
-rw-r--r-- | theories/Strings/vo.itarget | 2 | ||||
-rw-r--r-- | theories/Structures/vo.itarget | 14 | ||||
-rw-r--r-- | theories/Unicode/vo.itarget | 2 | ||||
-rw-r--r-- | theories/Vectors/vo.itarget | 5 | ||||
-rw-r--r-- | theories/Wellfounded/vo.itarget | 9 | ||||
-rw-r--r-- | theories/ZArith/vo.itarget | 33 |
24 files changed, 0 insertions, 390 deletions
diff --git a/theories/Arith/vo.itarget b/theories/Arith/vo.itarget deleted file mode 100644 index 0b3d31e98..000000000 --- a/theories/Arith/vo.itarget +++ /dev/null @@ -1,22 +0,0 @@ -PeanoNat.vo -Arith_base.vo -Arith.vo -Between.vo -Bool_nat.vo -Compare_dec.vo -Compare.vo -Div2.vo -EqNat.vo -Euclid.vo -Even.vo -Factorial.vo -Gt.vo -Le.vo -Lt.vo -Max.vo -Minus.vo -Min.vo -Mult.vo -Peano_dec.vo -Plus.vo -Wf_nat.vo diff --git a/theories/Bool/vo.itarget b/theories/Bool/vo.itarget deleted file mode 100644 index 24cbf4edc..000000000 --- a/theories/Bool/vo.itarget +++ /dev/null @@ -1,7 +0,0 @@ -BoolEq.vo -Bool.vo -Bvector.vo -DecBool.vo -IfProp.vo -Sumbool.vo -Zerob.vo diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget deleted file mode 100644 index 18147f2a4..000000000 --- a/theories/Classes/vo.itarget +++ /dev/null @@ -1,15 +0,0 @@ -DecidableClass.vo -Equivalence.vo -EquivDec.vo -Init.vo -Morphisms_Prop.vo -Morphisms_Relations.vo -Morphisms.vo -RelationClasses.vo -SetoidClass.vo -SetoidDec.vo -SetoidTactics.vo -RelationPairs.vo -CRelationClasses.vo -CMorphisms.vo -CEquivalence.vo diff --git a/theories/Compat/vo.itarget b/theories/Compat/vo.itarget deleted file mode 100644 index 7ffb86ebb..000000000 --- a/theories/Compat/vo.itarget +++ /dev/null @@ -1,4 +0,0 @@ -AdmitAxiom.vo -Coq84.vo -Coq85.vo -Coq86.vo diff --git a/theories/FSets/vo.itarget b/theories/FSets/vo.itarget deleted file mode 100644 index 0e7c11fb0..000000000 --- a/theories/FSets/vo.itarget +++ /dev/null @@ -1,21 +0,0 @@ -FMapAVL.vo -FMapFacts.vo -FMapFullAVL.vo -FMapInterface.vo -FMapList.vo -FMapPositive.vo -FMaps.vo -FMapWeakList.vo -FSetCompat.vo -FSetAVL.vo -FSetPositive.vo -FSetBridge.vo -FSetDecide.vo -FSetEqProperties.vo -FSetFacts.vo -FSetInterface.vo -FSetList.vo -FSetProperties.vo -FSets.vo -FSetToFiniteSet.vo -FSetWeakList.vo diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget deleted file mode 100644 index 99877065e..000000000 --- a/theories/Init/vo.itarget +++ /dev/null @@ -1,11 +0,0 @@ -Datatypes.vo -Logic_Type.vo -Logic.vo -Notations.vo -Peano.vo -Prelude.vo -Specif.vo -Tactics.vo -Wf.vo -Nat.vo -Tauto.vo diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget deleted file mode 100644 index 82dd1be82..000000000 --- a/theories/Lists/vo.itarget +++ /dev/null @@ -1,8 +0,0 @@ -ListSet.vo -ListTactics.vo -List.vo -ListDec.vo -SetoidList.vo -SetoidPermutation.vo -StreamMemo.vo -Streams.vo diff --git a/theories/MSets/vo.itarget b/theories/MSets/vo.itarget deleted file mode 100644 index 7c5b68995..000000000 --- a/theories/MSets/vo.itarget +++ /dev/null @@ -1,13 +0,0 @@ -MSetGenTree.vo -MSetAVL.vo -MSetRBT.vo -MSetDecide.vo -MSetEqProperties.vo -MSetFacts.vo -MSetInterface.vo -MSetList.vo -MSetProperties.vo -MSets.vo -MSetToFiniteSet.vo -MSetWeakList.vo -MSetPositive.vo
\ No newline at end of file diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget deleted file mode 100644 index e76033f78..000000000 --- a/theories/NArith/vo.itarget +++ /dev/null @@ -1,10 +0,0 @@ -BinNatDef.vo -BinNat.vo -NArith.vo -Ndec.vo -Ndigits.vo -Ndist.vo -Nnat.vo -Ndiv_def.vo -Nsqrt_def.vo -Ngcd_def.vo
\ No newline at end of file diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget deleted file mode 100644 index c69af03fc..000000000 --- a/theories/Numbers/vo.itarget +++ /dev/null @@ -1,91 +0,0 @@ -BinNums.vo -BigNumPrelude.vo -Cyclic/Abstract/CyclicAxioms.vo -Cyclic/Abstract/NZCyclic.vo -Cyclic/DoubleCyclic/DoubleAdd.vo -Cyclic/DoubleCyclic/DoubleBase.vo -Cyclic/DoubleCyclic/DoubleCyclic.vo -Cyclic/DoubleCyclic/DoubleDivn1.vo -Cyclic/DoubleCyclic/DoubleDiv.vo -Cyclic/DoubleCyclic/DoubleLift.vo -Cyclic/DoubleCyclic/DoubleMul.vo -Cyclic/DoubleCyclic/DoubleSqrt.vo -Cyclic/DoubleCyclic/DoubleSub.vo -Cyclic/DoubleCyclic/DoubleType.vo -Cyclic/Int31/Int31.vo -Cyclic/Int31/Cyclic31.vo -Cyclic/Int31/Ring31.vo -Cyclic/ZModulo/ZModulo.vo -Integer/Abstract/ZAddOrder.vo -Integer/Abstract/ZAdd.vo -Integer/Abstract/ZAxioms.vo -Integer/Abstract/ZBase.vo -Integer/Abstract/ZLt.vo -Integer/Abstract/ZMulOrder.vo -Integer/Abstract/ZMul.vo -Integer/Abstract/ZSgnAbs.vo -Integer/Abstract/ZDivFloor.vo -Integer/Abstract/ZDivTrunc.vo -Integer/Abstract/ZDivEucl.vo -Integer/Abstract/ZMaxMin.vo -Integer/Abstract/ZParity.vo -Integer/Abstract/ZPow.vo -Integer/Abstract/ZGcd.vo -Integer/Abstract/ZLcm.vo -Integer/Abstract/ZBits.vo -Integer/Abstract/ZProperties.vo -Integer/BigZ/BigZ.vo -Integer/BigZ/ZMake.vo -Integer/Binary/ZBinary.vo -Integer/NatPairs/ZNatPairs.vo -Integer/SpecViaZ/ZSig.vo -Integer/SpecViaZ/ZSigZAxioms.vo -NaryFunctions.vo -NatInt/NZAddOrder.vo -NatInt/NZAdd.vo -NatInt/NZAxioms.vo -NatInt/NZBase.vo -NatInt/NZMulOrder.vo -NatInt/NZMul.vo -NatInt/NZOrder.vo -NatInt/NZProperties.vo -NatInt/NZDomain.vo -NatInt/NZParity.vo -NatInt/NZDiv.vo -NatInt/NZPow.vo -NatInt/NZSqrt.vo -NatInt/NZLog.vo -NatInt/NZGcd.vo -NatInt/NZBits.vo -Natural/Abstract/NAddOrder.vo -Natural/Abstract/NAdd.vo -Natural/Abstract/NAxioms.vo -Natural/Abstract/NBase.vo -Natural/Abstract/NDefOps.vo -Natural/Abstract/NIso.vo -Natural/Abstract/NMulOrder.vo -Natural/Abstract/NOrder.vo -Natural/Abstract/NStrongRec.vo -Natural/Abstract/NSub.vo -Natural/Abstract/NProperties.vo -Natural/Abstract/NDiv.vo -Natural/Abstract/NMaxMin.vo -Natural/Abstract/NParity.vo -Natural/Abstract/NPow.vo -Natural/Abstract/NSqrt.vo -Natural/Abstract/NLog.vo -Natural/Abstract/NGcd.vo -Natural/Abstract/NLcm.vo -Natural/Abstract/NBits.vo -Natural/BigN/BigN.vo -Natural/BigN/Nbasic.vo -Natural/BigN/NMake_gen.vo -Natural/BigN/NMake.vo -Natural/Binary/NBinary.vo -Natural/Peano/NPeano.vo -Natural/SpecViaZ/NSigNAxioms.vo -Natural/SpecViaZ/NSig.vo -NumPrelude.vo -Rational/BigQ/BigQ.vo -Rational/BigQ/QMake.vo -Rational/SpecViaQ/QSig.vo diff --git a/theories/PArith/vo.itarget b/theories/PArith/vo.itarget deleted file mode 100644 index 73044e2c1..000000000 --- a/theories/PArith/vo.itarget +++ /dev/null @@ -1,5 +0,0 @@ -BinPosDef.vo -BinPos.vo -Pnat.vo -POrderedType.vo -PArith.vo
\ No newline at end of file diff --git a/theories/Program/vo.itarget b/theories/Program/vo.itarget deleted file mode 100644 index 864c815ae..000000000 --- a/theories/Program/vo.itarget +++ /dev/null @@ -1,9 +0,0 @@ -Basics.vo -Combinators.vo -Equality.vo -Program.vo -Subset.vo -Syntax.vo -Tactics.vo -Utils.vo -Wf.vo diff --git a/theories/QArith/vo.itarget b/theories/QArith/vo.itarget deleted file mode 100644 index b550b4712..000000000 --- a/theories/QArith/vo.itarget +++ /dev/null @@ -1,13 +0,0 @@ -Qabs.vo -QArith_base.vo -QArith.vo -Qcanon.vo -Qcabs.vo -Qfield.vo -Qpower.vo -Qreals.vo -Qreduction.vo -Qring.vo -Qround.vo -QOrderedType.vo -Qminmax.vo
\ No newline at end of file diff --git a/theories/Reals/vo.itarget b/theories/Reals/vo.itarget deleted file mode 100644 index 0c8f0b976..000000000 --- a/theories/Reals/vo.itarget +++ /dev/null @@ -1,62 +0,0 @@ -Alembert.vo -AltSeries.vo -ArithProp.vo -Binomial.vo -Cauchy_prod.vo -Cos_plus.vo -Cos_rel.vo -DiscrR.vo -Exp_prop.vo -Integration.vo -Machin.vo -MVT.vo -NewtonInt.vo -PartSum.vo -PSeries_reg.vo -Ranalysis1.vo -Ranalysis2.vo -Ranalysis3.vo -Ranalysis4.vo -Ranalysis5.vo -Ranalysis.vo -Ranalysis_reg.vo -Ratan.vo -Raxioms.vo -Rbase.vo -Rbasic_fun.vo -Rcomplete.vo -Rdefinitions.vo -Rderiv.vo -Reals.vo -Rfunctions.vo -Rgeom.vo -RiemannInt_SF.vo -RiemannInt.vo -R_Ifp.vo -RIneq.vo -Rlimit.vo -RList.vo -Rlogic.vo -Rpow_def.vo -Rpower.vo -Rprod.vo -Rseries.vo -Rsigma.vo -Rsqrt_def.vo -R_sqrt.vo -R_sqr.vo -Rtopology.vo -Rtrigo_alt.vo -Rtrigo_calc.vo -Rtrigo_def.vo -Rtrigo_fun.vo -Rtrigo_reg.vo -Rtrigo1.vo -Rtrigo.vo -SeqProp.vo -SeqSeries.vo -SplitAbsolu.vo -SplitRmult.vo -Sqrt_reg.vo -ROrderedType.vo -Rminmax.vo diff --git a/theories/Relations/vo.itarget b/theories/Relations/vo.itarget deleted file mode 100644 index 9d81dd07a..000000000 --- a/theories/Relations/vo.itarget +++ /dev/null @@ -1,4 +0,0 @@ -Operators_Properties.vo -Relation_Definitions.vo -Relation_Operators.vo -Relations.vo diff --git a/theories/Setoids/vo.itarget b/theories/Setoids/vo.itarget deleted file mode 100644 index 8d608cf75..000000000 --- a/theories/Setoids/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Setoid.vo
\ No newline at end of file diff --git a/theories/Sets/vo.itarget b/theories/Sets/vo.itarget deleted file mode 100644 index 9ebe92f52..000000000 --- a/theories/Sets/vo.itarget +++ /dev/null @@ -1,22 +0,0 @@ -Classical_sets.vo -Constructive_sets.vo -Cpo.vo -Ensembles.vo -Finite_sets_facts.vo -Finite_sets.vo -Image.vo -Infinite_sets.vo -Integers.vo -Multiset.vo -Partial_Order.vo -Permut.vo -Powerset_Classical_facts.vo -Powerset_facts.vo -Powerset.vo -Relations_1_facts.vo -Relations_1.vo -Relations_2_facts.vo -Relations_2.vo -Relations_3_facts.vo -Relations_3.vo -Uniset.vo diff --git a/theories/Sorting/vo.itarget b/theories/Sorting/vo.itarget deleted file mode 100644 index 079eaad18..000000000 --- a/theories/Sorting/vo.itarget +++ /dev/null @@ -1,7 +0,0 @@ -Heap.vo -Permutation.vo -PermutSetoid.vo -PermutEq.vo -Sorted.vo -Sorting.vo -Mergesort.vo diff --git a/theories/Strings/vo.itarget b/theories/Strings/vo.itarget deleted file mode 100644 index 20813b427..000000000 --- a/theories/Strings/vo.itarget +++ /dev/null @@ -1,2 +0,0 @@ -Ascii.vo -String.vo diff --git a/theories/Structures/vo.itarget b/theories/Structures/vo.itarget deleted file mode 100644 index 674e9fba9..000000000 --- a/theories/Structures/vo.itarget +++ /dev/null @@ -1,14 +0,0 @@ -Equalities.vo -EqualitiesFacts.vo -Orders.vo -OrdersEx.vo -OrdersFacts.vo -OrdersLists.vo -OrdersTac.vo -OrdersAlt.vo -GenericMinMax.vo -DecidableType.vo -DecidableTypeEx.vo -OrderedTypeAlt.vo -OrderedTypeEx.vo -OrderedType.vo diff --git a/theories/Unicode/vo.itarget b/theories/Unicode/vo.itarget deleted file mode 100644 index 7be1b9961..000000000 --- a/theories/Unicode/vo.itarget +++ /dev/null @@ -1,2 +0,0 @@ -Utf8.vo -Utf8_core.vo diff --git a/theories/Vectors/vo.itarget b/theories/Vectors/vo.itarget deleted file mode 100644 index 779b1821c..000000000 --- a/theories/Vectors/vo.itarget +++ /dev/null @@ -1,5 +0,0 @@ -Fin.vo -VectorDef.vo -VectorSpec.vo -VectorEq.vo -Vector.vo diff --git a/theories/Wellfounded/vo.itarget b/theories/Wellfounded/vo.itarget deleted file mode 100644 index 034d53106..000000000 --- a/theories/Wellfounded/vo.itarget +++ /dev/null @@ -1,9 +0,0 @@ -Disjoint_Union.vo -Inclusion.vo -Inverse_Image.vo -Lexicographic_Exponentiation.vo -Lexicographic_Product.vo -Transitive_Closure.vo -Union.vo -Wellfounded.vo -Well_Ordering.vo diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget deleted file mode 100644 index 178111cdf..000000000 --- a/theories/ZArith/vo.itarget +++ /dev/null @@ -1,33 +0,0 @@ -auxiliary.vo -BinIntDef.vo -BinInt.vo -Int.vo -Wf_Z.vo -Zabs.vo -ZArith_base.vo -ZArith_dec.vo -ZArith.vo -Zdigits.vo -Zbool.vo -Zcompare.vo -Zcomplements.vo -Zdiv.vo -Zeven.vo -Zgcd_alt.vo -Zpow_alt.vo -Zhints.vo -Zlogarithm.vo -Zmax.vo -Zminmax.vo -Zmin.vo -Zmisc.vo -Znat.vo -Znumtheory.vo -Zquot.vo -Zorder.vo -Zpow_def.vo -Zpower.vo -Zpow_facts.vo -Zsqrt_compat.vo -Zwf.vo -Zeuclid.vo |