matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 23 Aug 2008 13:18:57 +0000 (13:18 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 23 Aug 2008 13:18:57 +0000 (13:18 +0000)
commit	a89360d64f1fcbba917ad743b97a2d973ecf6db2
tree	f6806069e5c92c0e041ef8569c22f471ab2d9b4f	tree \| snapshot
parent	3e1e59644a24ed855a7f21bf9eab76f96577fd17	commit \| diff

Procedural: explicit flavour specification for constants is now working
            procedural inlining of inductive types is now working
    fixup in the generation of comments
grafiteAstPp: syntax fixup
transcript: now generates explicit flavour for inlined constants
            so we distinguish between definitions and theorems :)
    [the attributes are not present when we inline from Coq's library]
CoRN-Procedural: mma files regenerated with explicit flavours

160 files changed:

helm/software/components/acic_procedural/acic2Procedural.ml		diff \| blob \| history
helm/software/components/acic_procedural/proceduralTypes.ml		diff \| blob \| history
helm/software/components/acic_procedural/proceduralTypes.mli		diff \| blob \| history
helm/software/components/binaries/transcript/engine.ml		diff \| blob \| history
helm/software/components/binaries/transcript/grafite.ml		diff \| blob \| history
helm/software/components/binaries/transcript/types.ml		diff \| blob \| history
helm/software/components/binaries/transcript/v8Parser.mly		diff \| blob \| history
helm/software/components/grafite/grafiteAstPp.ml		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/Basics.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CAbGroups.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CAbMonoids.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CFields.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CGroups.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CLogic.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CMonoids.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/COrdAbs.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/COrdCauchy.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/COrdFields.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/COrdFields2.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CPoly_ApZero.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CPoly_Degree.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CPoly_NthCoeff.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CPolynomials.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CRings.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CSemiGroups.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CSetoidFun.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CSetoidInc.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CSetoids.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CSums.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/CVectorSpace.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/Cauchy_COF.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/Expon.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/algebra/ListType.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/complex/AbsCC.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/complex/CComplex.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/complex/Complex_Exponential.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/complex/NRootCC.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/devel/loeb/IDA/Ch6.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/devel/loeb/per/csetfun.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/devel/loeb/per/lst2fun.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/fta/CC_Props.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/fta/CPoly_Contin1.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/fta/CPoly_Rev.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/fta/CPoly_Shift.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/fta/FTA.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/fta/FTAreg.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/fta/KeyLemma.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/fta/KneserLemma.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/fta/MainLemma.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/COrdLemmas.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/CalculusTheorems.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/Composition.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/Continuity.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/Derivative.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/DerivativeOps.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/Differentiability.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/FTC.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/FunctSequence.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/FunctSeries.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/FunctSums.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/Integral.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/IntervalFunct.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/MoreFunSeries.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/MoreFunctions.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/MoreIntegrals.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/MoreIntervals.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/NthDerivative.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/PartFunEquality.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/PartInterval.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/Partitions.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/RefLemma.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/RefSepRef.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/RefSeparated.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/RefSeparating.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/Rolle.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/StrongIVT.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/Taylor.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/TaylorLemma.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/ftc/WeakIVT.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/metrics/CMetricSpaces.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/metrics/CPMSTheory.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/metrics/CPseudoMSpaces.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/metrics/ContFunctions.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/metrics/Equiv.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/metrics/IR_CPMSpace.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/metrics/Prod_Sub.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/abgroups/QSposabgroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Qabgroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Qposabgroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Zabgroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/fields/Qfield.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/groups/QSposgroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/groups/Qgroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/groups/Qposgroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/groups/Zgroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/monoids/Nmonoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/monoids/Nposmonoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/monoids/QSposmonoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/monoids/Qmonoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/monoids/Qposmonoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/monoids/Zmonoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/non_examples/N_no_group.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/non_examples/Npos_no_group.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/non_examples/Npos_no_monoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/ordfields/Qordfield.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/reals/Cauchy_IR.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/rings/Qring.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/rings/Zring.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/semigroups/Npossemigroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/semigroups/Nsemigroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/semigroups/QSpossemigroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/semigroups/Qpossemigroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/semigroups/Qsemigroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/semigroups/Zsemigroup.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/setoids/Npossetoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/setoids/Nsetoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/setoids/Qpossetoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/setoids/Qsetoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/setoids/Zsetoid.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/structures/Npossec.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/structures/Nsec.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/structures/Qpossec.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/structures/Qsec.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/model/structures/Zsec.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/Bridges_LUB.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/Bridges_iso.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/CMetricFields.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/CPoly_Contin.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/CReals.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/CReals1.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/CSumsReals.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/CauchySeq.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/Cauchy_CReals.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/IVT.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/Intervals.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/Max_AbsIR.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/NRootIR.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/OddPolyRootIR.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/Q_dense.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/Q_in_CReals.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/R_morphism.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/RealFuncts.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/RealLists.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/reals/iso_CReals.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/tactics/AlgReflection.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/tactics/DiffTactics2.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/tactics/DiffTactics3.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/tactics/FieldReflection.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/tactics/GroupReflection.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/tactics/RingReflection.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/transc/Exponential.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/transc/InvTrigonom.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/transc/Pi.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/transc/PowerSeries.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/transc/RealPowers.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/transc/SinCos.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/transc/TaylorSeries.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/transc/TrigMon.mma		diff \| blob \| history
helm/software/matita/contribs/CoRN-Procedural/transc/Trigonometric.mma		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom