]> matita.cs.unibo.it Git - helm.git/commit - helm/software/matita/contribs/procedural/Coq/Wellfounded/Lexicographic_Exponentiation.mma
transcript: we now check for non-existing objects
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 5 Sep 2008 18:37:01 +0000 (18:37 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 5 Sep 2008 18:37:01 +0000 (18:37 +0000)
commitf620bf94af6c347926ed1c2328462efab7018b21
tree9fde04b63b99abecb50eb0e396ef7243a869f2ba
parent418b1f26ab67b824c79d1146fdb50ca29b34c1f6
transcript: we now check for non-existing objects
procedural/Coq: we now generate from ufficial 8.0pl2
                that does not have the Num directory
235 files changed:
helm/software/components/binaries/transcript/.depend.opt
helm/software/components/binaries/transcript/engine.ml
helm/software/components/binaries/transcript/engine.mli
helm/software/components/binaries/transcript/grafite.ml
helm/software/components/binaries/transcript/options.ml
helm/software/components/binaries/transcript/top.ml
helm/software/components/binaries/transcript/v8Parser.mly
helm/software/matita/contribs/procedural/Coq/Arith/Arith.mma
helm/software/matita/contribs/procedural/Coq/Arith/Between.mma
helm/software/matita/contribs/procedural/Coq/Arith/Bool_nat.mma
helm/software/matita/contribs/procedural/Coq/Arith/Compare.mma
helm/software/matita/contribs/procedural/Coq/Arith/Compare_dec.mma
helm/software/matita/contribs/procedural/Coq/Arith/Div.mma
helm/software/matita/contribs/procedural/Coq/Arith/Div2.mma
helm/software/matita/contribs/procedural/Coq/Arith/EqNat.mma
helm/software/matita/contribs/procedural/Coq/Arith/Euclid.mma
helm/software/matita/contribs/procedural/Coq/Arith/Even.mma
helm/software/matita/contribs/procedural/Coq/Arith/Factorial.mma
helm/software/matita/contribs/procedural/Coq/Arith/Gt.mma
helm/software/matita/contribs/procedural/Coq/Arith/Le.mma
helm/software/matita/contribs/procedural/Coq/Arith/Lt.mma
helm/software/matita/contribs/procedural/Coq/Arith/Max.mma
helm/software/matita/contribs/procedural/Coq/Arith/Min.mma
helm/software/matita/contribs/procedural/Coq/Arith/Minus.mma
helm/software/matita/contribs/procedural/Coq/Arith/Mult.mma
helm/software/matita/contribs/procedural/Coq/Arith/Peano_dec.mma
helm/software/matita/contribs/procedural/Coq/Arith/Plus.mma
helm/software/matita/contribs/procedural/Coq/Arith/Wf_nat.mma
helm/software/matita/contribs/procedural/Coq/Bool/Bool.mma
helm/software/matita/contribs/procedural/Coq/Bool/BoolEq.mma
helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma
helm/software/matita/contribs/procedural/Coq/Bool/DecBool.mma
helm/software/matita/contribs/procedural/Coq/Bool/IfProp.mma
helm/software/matita/contribs/procedural/Coq/Bool/Sumbool.mma
helm/software/matita/contribs/procedural/Coq/Bool/Zerob.mma
helm/software/matita/contribs/procedural/Coq/Coq.conf.xml
helm/software/matita/contribs/procedural/Coq/Coq.ma
helm/software/matita/contribs/procedural/Coq/Init/Datatypes.mma
helm/software/matita/contribs/procedural/Coq/Init/Logic.mma
helm/software/matita/contribs/procedural/Coq/Init/Logic_Type.mma
helm/software/matita/contribs/procedural/Coq/Init/Notations.mma
helm/software/matita/contribs/procedural/Coq/Init/Peano.mma
helm/software/matita/contribs/procedural/Coq/Init/Prelude.mma
helm/software/matita/contribs/procedural/Coq/Init/Specif.mma
helm/software/matita/contribs/procedural/Coq/Init/Wf.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Adalloc.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Addec.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Addr.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Adist.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Allmaps.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Fset.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Lsort.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Map.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Mapaxioms.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Mapc.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Mapcanon.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Mapcard.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Mapfold.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Mapiter.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Maplists.mma
helm/software/matita/contribs/procedural/Coq/IntMap/Mapsubset.mma
helm/software/matita/contribs/procedural/Coq/Lists/List.mma
helm/software/matita/contribs/procedural/Coq/Lists/ListSet.mma
helm/software/matita/contribs/procedural/Coq/Lists/MonoList.mma
helm/software/matita/contribs/procedural/Coq/Lists/Streams.mma [new file with mode: 0644]
helm/software/matita/contribs/procedural/Coq/Lists/TheoryList.mma
helm/software/matita/contribs/procedural/Coq/Logic/Berardi.mma
helm/software/matita/contribs/procedural/Coq/Logic/ChoiceFacts.mma
helm/software/matita/contribs/procedural/Coq/Logic/Classical.mma
helm/software/matita/contribs/procedural/Coq/Logic/ClassicalChoice.mma
helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma
helm/software/matita/contribs/procedural/Coq/Logic/ClassicalFacts.mma
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Pred_Set.mma
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Pred_Type.mma
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Prop.mma
helm/software/matita/contribs/procedural/Coq/Logic/Classical_Type.mma
helm/software/matita/contribs/procedural/Coq/Logic/Decidable.mma
helm/software/matita/contribs/procedural/Coq/Logic/Diaconescu.mma
helm/software/matita/contribs/procedural/Coq/Logic/Eqdep.mma
helm/software/matita/contribs/procedural/Coq/Logic/Eqdep_dec.mma
helm/software/matita/contribs/procedural/Coq/Logic/Hurkens.mma
helm/software/matita/contribs/procedural/Coq/Logic/JMeq.mma
helm/software/matita/contribs/procedural/Coq/Logic/ProofIrrelevance.mma
helm/software/matita/contribs/procedural/Coq/Logic/RelationalChoice.mma
helm/software/matita/contribs/procedural/Coq/NArith/BinNat.mma
helm/software/matita/contribs/procedural/Coq/NArith/BinPos.mma
helm/software/matita/contribs/procedural/Coq/NArith/NArith.mma
helm/software/matita/contribs/procedural/Coq/NArith/Pnat.mma
helm/software/matita/contribs/procedural/Coq/Num/AddProps.mma
helm/software/matita/contribs/procedural/Coq/Num/Axioms.mma
helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma
helm/software/matita/contribs/procedural/Coq/Num/DiscrAxioms.mma
helm/software/matita/contribs/procedural/Coq/Num/DiscrProps.mma
helm/software/matita/contribs/procedural/Coq/Num/EqAxioms.mma
helm/software/matita/contribs/procedural/Coq/Num/EqParams.mma
helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma
helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma
helm/software/matita/contribs/procedural/Coq/Num/GtAxioms.mma
helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma
helm/software/matita/contribs/procedural/Coq/Num/LeAxioms.mma
helm/software/matita/contribs/procedural/Coq/Num/LeProps.mma
helm/software/matita/contribs/procedural/Coq/Num/Leibniz/EqAxioms.mma
helm/software/matita/contribs/procedural/Coq/Num/Leibniz/NSyntax.mma
helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma
helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma
helm/software/matita/contribs/procedural/Coq/Num/NSyntax.mma
helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma
helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma
helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma
helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma
helm/software/matita/contribs/procedural/Coq/Num/NeqDef.mma
helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma
helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma
helm/software/matita/contribs/procedural/Coq/Num/OppAxioms.mma
helm/software/matita/contribs/procedural/Coq/Num/OppProps.mma
helm/software/matita/contribs/procedural/Coq/Num/Params.mma
helm/software/matita/contribs/procedural/Coq/Num/SubProps.mma
helm/software/matita/contribs/procedural/Coq/Reals/Alembert.mma
helm/software/matita/contribs/procedural/Coq/Reals/AltSeries.mma
helm/software/matita/contribs/procedural/Coq/Reals/ArithProp.mma
helm/software/matita/contribs/procedural/Coq/Reals/Binomial.mma
helm/software/matita/contribs/procedural/Coq/Reals/Cauchy_prod.mma
helm/software/matita/contribs/procedural/Coq/Reals/Cos_plus.mma
helm/software/matita/contribs/procedural/Coq/Reals/Cos_rel.mma
helm/software/matita/contribs/procedural/Coq/Reals/DiscrR.mma
helm/software/matita/contribs/procedural/Coq/Reals/Exp_prop.mma
helm/software/matita/contribs/procedural/Coq/Reals/Integration.mma
helm/software/matita/contribs/procedural/Coq/Reals/MVT.mma
helm/software/matita/contribs/procedural/Coq/Reals/NewtonInt.mma
helm/software/matita/contribs/procedural/Coq/Reals/PSeries_reg.mma
helm/software/matita/contribs/procedural/Coq/Reals/PartSum.mma
helm/software/matita/contribs/procedural/Coq/Reals/RIneq.mma
helm/software/matita/contribs/procedural/Coq/Reals/RList.mma
helm/software/matita/contribs/procedural/Coq/Reals/R_Ifp.mma
helm/software/matita/contribs/procedural/Coq/Reals/R_sqr.mma
helm/software/matita/contribs/procedural/Coq/Reals/R_sqrt.mma
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis.mma
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis1.mma
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis2.mma
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis3.mma
helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis4.mma
helm/software/matita/contribs/procedural/Coq/Reals/Raxioms.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rbase.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rbasic_fun.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rcomplete.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rdefinitions.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rderiv.mma
helm/software/matita/contribs/procedural/Coq/Reals/Reals.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rfunctions.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rgeom.mma
helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt.mma
helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt_SF.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rlimit.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rpower.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rseries.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rsigma.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rsqrt_def.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rtopology.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_alt.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_calc.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_def.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_fun.mma
helm/software/matita/contribs/procedural/Coq/Reals/Rtrigo_reg.mma
helm/software/matita/contribs/procedural/Coq/Reals/SeqProp.mma
helm/software/matita/contribs/procedural/Coq/Reals/SeqSeries.mma
helm/software/matita/contribs/procedural/Coq/Reals/SplitAbsolu.mma
helm/software/matita/contribs/procedural/Coq/Reals/SplitRmult.mma
helm/software/matita/contribs/procedural/Coq/Reals/Sqrt_reg.mma
helm/software/matita/contribs/procedural/Coq/Relations/Newman.mma
helm/software/matita/contribs/procedural/Coq/Relations/Operators_Properties.mma
helm/software/matita/contribs/procedural/Coq/Relations/Relation_Definitions.mma
helm/software/matita/contribs/procedural/Coq/Relations/Relation_Operators.mma
helm/software/matita/contribs/procedural/Coq/Relations/Relations.mma
helm/software/matita/contribs/procedural/Coq/Relations/Rstar.mma
helm/software/matita/contribs/procedural/Coq/Setoids/Setoid.mma
helm/software/matita/contribs/procedural/Coq/Sets/Classical_sets.mma
helm/software/matita/contribs/procedural/Coq/Sets/Constructive_sets.mma
helm/software/matita/contribs/procedural/Coq/Sets/Cpo.mma
helm/software/matita/contribs/procedural/Coq/Sets/Ensembles.mma
helm/software/matita/contribs/procedural/Coq/Sets/Finite_sets.mma
helm/software/matita/contribs/procedural/Coq/Sets/Finite_sets_facts.mma
helm/software/matita/contribs/procedural/Coq/Sets/Image.mma
helm/software/matita/contribs/procedural/Coq/Sets/Infinite_sets.mma
helm/software/matita/contribs/procedural/Coq/Sets/Integers.mma
helm/software/matita/contribs/procedural/Coq/Sets/Multiset.mma
helm/software/matita/contribs/procedural/Coq/Sets/Partial_Order.mma
helm/software/matita/contribs/procedural/Coq/Sets/Permut.mma
helm/software/matita/contribs/procedural/Coq/Sets/Powerset.mma
helm/software/matita/contribs/procedural/Coq/Sets/Powerset_Classical_facts.mma
helm/software/matita/contribs/procedural/Coq/Sets/Powerset_facts.mma
helm/software/matita/contribs/procedural/Coq/Sets/Relations_1.mma
helm/software/matita/contribs/procedural/Coq/Sets/Relations_1_facts.mma
helm/software/matita/contribs/procedural/Coq/Sets/Relations_2.mma
helm/software/matita/contribs/procedural/Coq/Sets/Relations_2_facts.mma
helm/software/matita/contribs/procedural/Coq/Sets/Relations_3.mma
helm/software/matita/contribs/procedural/Coq/Sets/Relations_3_facts.mma
helm/software/matita/contribs/procedural/Coq/Sets/Uniset.mma
helm/software/matita/contribs/procedural/Coq/Sorting/Heap.mma
helm/software/matita/contribs/procedural/Coq/Sorting/Permutation.mma
helm/software/matita/contribs/procedural/Coq/Sorting/Sorting.mma
helm/software/matita/contribs/procedural/Coq/Wellfounded/Disjoint_Union.mma
helm/software/matita/contribs/procedural/Coq/Wellfounded/Inclusion.mma
helm/software/matita/contribs/procedural/Coq/Wellfounded/Inverse_Image.mma
helm/software/matita/contribs/procedural/Coq/Wellfounded/Lexicographic_Exponentiation.mma
helm/software/matita/contribs/procedural/Coq/Wellfounded/Lexicographic_Product.mma
helm/software/matita/contribs/procedural/Coq/Wellfounded/Transitive_Closure.mma
helm/software/matita/contribs/procedural/Coq/Wellfounded/Union.mma
helm/software/matita/contribs/procedural/Coq/Wellfounded/Well_Ordering.mma
helm/software/matita/contribs/procedural/Coq/Wellfounded/Wellfounded.mma
helm/software/matita/contribs/procedural/Coq/ZArith/BinInt.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Wf_Z.mma
helm/software/matita/contribs/procedural/Coq/ZArith/ZArith.mma
helm/software/matita/contribs/procedural/Coq/ZArith/ZArith_base.mma
helm/software/matita/contribs/procedural/Coq/ZArith/ZArith_dec.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zabs.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zbool.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zcompare.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zcomplements.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zdiv.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zeven.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zhints.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zlogarithm.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zmin.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zmisc.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Znat.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Znumtheory.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zorder.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zpower.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zsqrt.mma
helm/software/matita/contribs/procedural/Coq/ZArith/Zwf.mma
helm/software/matita/contribs/procedural/Coq/ZArith/auxiliary.mma
helm/software/matita/contribs/procedural/Makefile.common