aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2017-03-23 12:56:24 +0100
committerGravatar Matej Kosik <matej.kosik@inria.fr>2017-06-01 17:33:19 +0200
commit718d61a54157733bca61ed84c0ba3761cd52720f (patch)
tree4c57fa4ad6d75c5fc4f5747289dfed82d83dfc9a /theories
parent7fff12d45c4d86fa5cb9be3883084ffef5911405 (diff)
drop vo.itarget files and compute the corresponding the corresponding values automatically instead
Diffstat (limited to 'theories')
-rw-r--r--theories/Arith/vo.itarget22
-rw-r--r--theories/Bool/vo.itarget7
-rw-r--r--theories/Classes/vo.itarget15
-rw-r--r--theories/Compat/vo.itarget4
-rw-r--r--theories/FSets/vo.itarget21
-rw-r--r--theories/Init/vo.itarget11
-rw-r--r--theories/Lists/vo.itarget8
-rw-r--r--theories/MSets/vo.itarget13
-rw-r--r--theories/NArith/vo.itarget10
-rw-r--r--theories/Numbers/vo.itarget91
-rw-r--r--theories/PArith/vo.itarget5
-rw-r--r--theories/Program/vo.itarget9
-rw-r--r--theories/QArith/vo.itarget13
-rw-r--r--theories/Reals/vo.itarget62
-rw-r--r--theories/Relations/vo.itarget4
-rw-r--r--theories/Setoids/vo.itarget1
-rw-r--r--theories/Sets/vo.itarget22
-rw-r--r--theories/Sorting/vo.itarget7
-rw-r--r--theories/Strings/vo.itarget2
-rw-r--r--theories/Structures/vo.itarget14
-rw-r--r--theories/Unicode/vo.itarget2
-rw-r--r--theories/Vectors/vo.itarget5
-rw-r--r--theories/Wellfounded/vo.itarget9
-rw-r--r--theories/ZArith/vo.itarget33
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