Andrea Asperti [Wed, 29 Nov 2006 08:00:09 +0000 (08:00 +0000)]
Demodulate_tac now depends on the universe
Claudio Sacerdoti Coen [Tue, 28 Nov 2006 18:57:26 +0000 (18:57 +0000)]
Added a clear to rewritestep to speed up auto (by removing an hypothesis
that must NOT be used again).
Andrea Asperti [Tue, 28 Nov 2006 17:47:31 +0000 (17:47 +0000)]
Changed an ahstable into an association list.
Claudio Sacerdoti Coen [Mon, 27 Nov 2006 16:50:15 +0000 (16:50 +0000)]
"the thesis becomes" now always performs a change.
Claudio Sacerdoti Coen [Mon, 27 Nov 2006 15:01:04 +0000 (15:01 +0000)]
Fixed bug in notation: when a notation is applied to more arguments than expected this is not necessarily a problem: I just create a new application on the fly.
Andrea Asperti [Mon, 27 Nov 2006 13:48:35 +0000 (13:48 +0000)]
Added in_eq_uris.
Andrea Asperti [Mon, 27 Nov 2006 13:46:19 +0000 (13:46 +0000)]
Fix_proof should recursively work on explicit substs.
For the moment this is done for constants.
Claudio Sacerdoti Coen [Mon, 27 Nov 2006 13:45:51 +0000 (13:45 +0000)]
Declarative language ported to new auto (with Universes).
Andrea Asperti [Mon, 27 Nov 2006 12:54:42 +0000 (12:54 +0000)]
Removed a couple of assertions.
Andrea Asperti [Mon, 27 Nov 2006 12:52:53 +0000 (12:52 +0000)]
Commented an assertion.
Andrea Asperti [Mon, 27 Nov 2006 12:50:14 +0000 (12:50 +0000)]
Commented an assertion.
Andrea Asperti [Mon, 27 Nov 2006 12:42:03 +0000 (12:42 +0000)]
Commented a few assertions.
Andrea Asperti [Mon, 27 Nov 2006 12:32:11 +0000 (12:32 +0000)]
Variant are not indexed.
Andrea Asperti [Mon, 27 Nov 2006 12:31:26 +0000 (12:31 +0000)]
Only modified for taking unfold into account.
Assertion made only in case of debug.
Andrea Asperti [Mon, 27 Nov 2006 12:20:35 +0000 (12:20 +0000)]
Matita's default equality has changed
-This line, and those below, will be ignored--
M library/logic/equality.ma
Andrea Asperti [Mon, 27 Nov 2006 11:59:16 +0000 (11:59 +0000)]
Small changes
Claudio Sacerdoti Coen [Mon, 27 Nov 2006 10:44:18 +0000 (10:44 +0000)]
auto new => auto new library in those tests that use Coq's library
Enrico Tassi [Sat, 25 Nov 2006 11:57:01 +0000 (11:57 +0000)]
fix
Enrico Tassi [Sat, 25 Nov 2006 11:27:26 +0000 (11:27 +0000)]
patch to calculate meets of a pair of carriers
Enrico Tassi [Sat, 25 Nov 2006 11:26:09 +0000 (11:26 +0000)]
added assertion (that is a TODO) in case non-considered exceptions are raised when tring to apply coercions
Enrico Tassi [Sat, 25 Nov 2006 11:23:02 +0000 (11:23 +0000)]
added a test for the pullback stuff and the possibility to get the coercion graph printed without closures
Andrea Asperti [Thu, 23 Nov 2006 14:46:01 +0000 (14:46 +0000)]
Command index added to disambiguate.
-This line, and those below, will be ignored--
M grafite_parser/grafiteDisambiguate.ml
Andrea Asperti [Thu, 23 Nov 2006 14:44:48 +0000 (14:44 +0000)]
Added a new command "index" for the indexing terms in the "universe".
Andrea Asperti [Thu, 23 Nov 2006 14:41:25 +0000 (14:41 +0000)]
Set of Set of uri added.
Andrea Asperti [Thu, 23 Nov 2006 14:31:56 +0000 (14:31 +0000)]
Modifications to auto due to the introduction of the universe in
the status.
Andrea Asperti [Thu, 23 Nov 2006 14:09:08 +0000 (14:09 +0000)]
Universe is a discrimination-tree structure.
Andrea Asperti [Thu, 23 Nov 2006 14:06:57 +0000 (14:06 +0000)]
The status has been extended with a "universe", that is a
discrimination-tree structure indexing all defined objects.
The universe is functional (hope so).
Andrea Asperti [Thu, 23 Nov 2006 13:56:30 +0000 (13:56 +0000)]
Fixed a call to auto, and commented the remaining part.
Andrea Asperti [Thu, 23 Nov 2006 13:46:27 +0000 (13:46 +0000)]
paramodulation removed
Andrea Asperti [Thu, 23 Nov 2006 13:45:53 +0000 (13:45 +0000)]
Minor changes.
-This line, and those below, will be ignored--
M library/nat/ord.ma
M library/nat/gcd.ma
M library/nat/factorization.ma
M library/technicalities/setoids.ma
Andrea Asperti [Thu, 23 Nov 2006 13:03:45 +0000 (13:03 +0000)]
Simplified version.
Andrea Asperti [Thu, 23 Nov 2006 09:33:24 +0000 (09:33 +0000)]
Adding CoRN.
Ferruccio Guidi [Wed, 22 Nov 2006 15:24:20 +0000 (15:24 +0000)]
removed the impredicativity of falsum
Claudio Sacerdoti Coen [Fri, 17 Nov 2006 18:39:43 +0000 (18:39 +0000)]
Fixed the infamous bug:
> >/home/sacerdot/miohelm/matita/scripts/crontab.sh: line 70: [: : integer
> >expression expected
Ferruccio Guidi [Fri, 17 Nov 2006 18:20:47 +0000 (18:20 +0000)]
helm_registry: added the pair unmarshaller
grafiteAstPp: bug-fixed
transcript: coercion handling improved
CoRN-Decl: regenerated accordingly
--ehis line, and those below, will be ignored--
M software/matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma
M software/matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma
M software/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma
M software/matita/contribs/CoRN-Decl/model/groups/Zgroup.ma
M software/matita/contribs/CoRN-Decl/model/groups/Qgroup.ma
M software/matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma
M software/matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma
M software/matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma
M software/matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma
M software/matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma
M software/matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma
M software/matita/contribs/CoRN-Decl/model/rings/Zring.ma
M software/matita/contribs/CoRN-Decl/model/rings/Qring.ma
M software/matita/contribs/CoRN-Decl/model/structures/Zsec.ma
M software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma
M software/matita/contribs/CoRN-Decl/model/structures/Npossec.ma
M software/matita/contribs/CoRN-Decl/model/structures/Qsec.ma
M software/matita/contribs/CoRN-Decl/model/structures/Qpossec.ma
M software/matita/contribs/CoRN-Decl/model/fields/Qfield.ma
M software/matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma
M software/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma
M software/matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma
M software/matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma
M software/matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma
M software/matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma
M software/matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma
M software/matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma
M software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma
M software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma
M software/matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma
M software/matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma
M software/matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma
M software/matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma
M software/matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma
M software/matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma
M software/matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma
M software/matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma
M software/matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma
M software/matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma
M software/matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma
M software/matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma
M software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
M software/matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma
M software/matita/contribs/CoRN-Decl/metrics/Equiv.ma
M software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
M software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
M software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
M software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
M software/matita/contribs/CoRN-Decl/reals/iso_CReals.ma
M software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
M software/matita/contribs/CoRN-Decl/reals/Bridges_iso.ma
M software/matita/contribs/CoRN-Decl/reals/CReals1.ma
M software/matita/contribs/CoRN-Decl/reals/Series.ma
M software/matita/contribs/CoRN-Decl/reals/NRootIR.ma
M software/matita/contribs/CoRN-Decl/reals/CPoly_Contin.ma
M software/matita/contribs/CoRN-Decl/reals/IVT.ma
M software/matita/contribs/CoRN-Decl/reals/RealLists.ma
M software/matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma
M software/matita/contribs/CoRN-Decl/reals/Cauchy_CReals.ma
M software/matita/contribs/CoRN-Decl/reals/RealFuncts.ma
M software/matita/contribs/CoRN-Decl/reals/Intervals.ma
M software/matita/contribs/CoRN-Decl/reals/OddPolyRootIR.ma
M software/matita/contribs/CoRN-Decl/reals/CReals.ma
M software/matita/contribs/CoRN-Decl/reals/CMetricFields.ma
M software/matita/contribs/CoRN-Decl/reals/Q_dense.ma
M software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma
M software/matita/contribs/CoRN-Decl/reals/R_morphism.ma
M software/matita/contribs/CoRN-Decl/reals/CSumsReals.ma
M software/matita/contribs/CoRN-Decl/reals/Bridges_LUB.ma
M software/matita/contribs/CoRN-Decl/complex/NRootCC.ma
M software/matita/contribs/CoRN-Decl/complex/CComplex.ma
M software/matita/contribs/CoRN-Decl/complex/AbsCC.ma
M software/matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma
D software/matita/contribs/CoRN-Decl/CoRN_notation.ma
M software/matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma
M software/matita/contribs/CoRN-Decl/fta/KneserLemma.ma
M software/matita/contribs/CoRN-Decl/fta/KeyLemma.ma
M software/matita/contribs/CoRN-Decl/fta/CC_Props.ma
M software/matita/contribs/CoRN-Decl/fta/FTAreg.ma
M software/matita/contribs/CoRN-Decl/fta/FTA.ma
M software/matita/contribs/CoRN-Decl/fta/MainLemma.ma
M software/matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma
M software/matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma
M software/matita/contribs/CoRN-Decl/tactics/DiffTactics1.ma
M software/matita/contribs/CoRN-Decl/tactics/DiffTactics2.ma
M software/matita/contribs/CoRN-Decl/tactics/DiffTactics3.ma
M software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma
M software/matita/contribs/CoRN-Decl/tactics/Opaque_algebra.ma
M software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma
M software/matita/contribs/CoRN-Decl/tactics/Step.ma
M software/matita/contribs/CoRN-Decl/tactics/AlgReflection.ma
M software/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma
M software/matita/contribs/CoRN-Decl/tactics/Transparent_algebra.ma
M software/matita/contribs/CoRN-Decl/transc/RealPowers.ma
M software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma
M software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma
M software/matita/contribs/CoRN-Decl/transc/Exponential.ma
M software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma
M software/matita/contribs/CoRN-Decl/transc/Pi.ma
M software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma
M software/matita/contribs/CoRN-Decl/transc/SinCos.ma
M software/matita/contribs/CoRN-Decl/transc/TrigMon.ma
M software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma
M software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma
M software/matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma
M software/matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma
M software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma
M software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma
M software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma
M software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma
M software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma
M software/matita/contribs/CoRN-Decl/ftc/RefSeparating.ma
M software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma
M software/matita/contribs/CoRN-Decl/ftc/Partitions.ma
M software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma
M software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma
M software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma
M software/matita/contribs/CoRN-Decl/ftc/Derivative.ma
M software/matita/contribs/CoRN-Decl/ftc/Composition.ma
M software/matita/contribs/CoRN-Decl/ftc/Integral.ma
M software/matita/contribs/CoRN-Decl/ftc/Continuity.ma
M software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma
M software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma
M software/matita/contribs/CoRN-Decl/ftc/Taylor.ma
M software/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma
M software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma
M software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
M software/matita/contribs/CoRN-Decl/ftc/FTC.ma
M software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma
M software/matita/contribs/CoRN-Decl/ftc/Rolle.ma
M software/matita/contribs/CoRN-Decl/ftc/RefSepRef.ma
M software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
M software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma
M software/matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma
M software/matita/contribs/CoRN-Decl/algebra/CAbGroups.ma
M software/matita/contribs/CoRN-Decl/algebra/CRings.ma
M software/matita/contribs/CoRN-Decl/algebra/Expon.ma
M software/matita/contribs/CoRN-Decl/algebra/CSums.ma
M software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma
M software/matita/contribs/CoRN-Decl/algebra/CLogic.ma
M software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
M software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma
M software/matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma
M software/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma
M software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma
M software/matita/contribs/CoRN-Decl/algebra/Basics.ma
M software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma
M software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma
M software/matita/contribs/CoRN-Decl/algebra/CFields.ma
M software/matita/contribs/CoRN-Decl/algebra/CMonoids.ma
M software/matita/contribs/CoRN-Decl/algebra/COrdAbs.ma
M software/matita/contribs/CoRN-Decl/algebra/CSetoids.ma
M software/matita/contribs/CoRN-Decl/algebra/ListType.ma
M software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma
M software/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma
M software/matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma
M software/matita/contribs/CoRN-Decl/algebra/CGroups.ma
A software/matita/contribs/CoRN-Decl/CoRN.ma
M software/components/grafite/grafiteAstPp.ml
M software/components/binaries/transcript/CoRN.conf.xml
M software/components/binaries/transcript/grafite.ml
M software/components/binaries/transcript/v8Parser.mly
M software/components/binaries/transcript/types.ml
M software/components/binaries/transcript/engine.ml
M software/components/registry/helm_registry.ml
M software/components/registry/helm_registry.mli
Ferruccio Guidi [Fri, 17 Nov 2006 10:16:10 +0000 (10:16 +0000)]
CoRN-Decl: missing file added
Ferruccio Guidi [Thu, 16 Nov 2006 15:12:17 +0000 (15:12 +0000)]
- transcript: patched to generate CoRN_notation.ma instead of CoRN.ma
- CoRN-Decl: regenerated
Ferruccio Guidi [Thu, 16 Nov 2006 14:45:39 +0000 (14:45 +0000)]
- transcript: now outputs includes and coercions correctly
- GrafiteAstPp: coercion and inline pretty printing patched
- CoRN-Decl: regenerated: starts to compile :) but inline is broken :(
Ferruccio Guidi [Wed, 15 Nov 2006 19:52:45 +0000 (19:52 +0000)]
new CoRN development, generated by transcript
Ferruccio Guidi [Wed, 15 Nov 2006 19:47:41 +0000 (19:47 +0000)]
transcript updated
Ferruccio Guidi [Wed, 15 Nov 2006 14:11:51 +0000 (14:11 +0000)]
removed prived CoRN configuration file :)
Ferruccio Guidi [Wed, 15 Nov 2006 14:10:33 +0000 (14:10 +0000)]
transcript: very alpha version.
parser for Coq V8 works fine on CoRN contribution scripts.
Ferruccio Guidi [Wed, 15 Nov 2006 13:03:37 +0000 (13:03 +0000)]
fixed base uri
Andrea Asperti [Wed, 15 Nov 2006 09:09:02 +0000 (09:09 +0000)]
lt_O_S moved to nat/orders.ma
Andrea Asperti [Wed, 15 Nov 2006 09:06:10 +0000 (09:06 +0000)]
Added lt_O_S.
Claudio Sacerdoti Coen [Tue, 14 Nov 2006 15:36:41 +0000 (15:36 +0000)]
&TODO => &TODO;
maiorino [Tue, 14 Nov 2006 15:30:25 +0000 (15:30 +0000)]
New: on-line help for declarative tactics (first version).
Claudio Sacerdoti Coen [Tue, 14 Nov 2006 14:48:54 +0000 (14:48 +0000)]
library=1 in obtain _ = _ by _.
Claudio Sacerdoti Coen [Sun, 12 Nov 2006 18:58:56 +0000 (18:58 +0000)]
The pretty printers in CicPp now have an optional ~metasenv argument to
show the globally restricted arguments of a metavariable local context as
locally restricted. The pretty printers in CicMetaSubst have the same argument,
but the argument is mandatory.
Ferruccio Guidi [Sat, 11 Nov 2006 18:53:10 +0000 (18:53 +0000)]
NLE is now derived fron NPlus rather than being a stand-alone relation
Enrico Zoli [Fri, 10 Nov 2006 18:06:13 +0000 (18:06 +0000)]
Dama: up to L-spaces and the proof (completed up to properties of the
absolute value) that every complete integration riesz space is an L-space.
Now the plan is to prove the Lebesgue dominated convergence theorem for
L-spaces as Fremlin does and to build a model of them later on as suggested
by Spitters. Note: the proof of the theorem by Spitters is almost trivial
because it really exploits the fact the L0 is the (Cauchy) completion of L1.
The proof by Fremlin is much more general since it does not assume anything
more on L-spaces.
Note: we could also prove that every L-space is archimedean.
Enrico Zoli [Mon, 6 Nov 2006 18:43:24 +0000 (18:43 +0000)]
More work on groups, real numbers and integration algebras.
Up to a thousand of unproved lemmas, we have the result that the
distance induced by the integral on an integration Riesz space is
a distance. The next step is to axiomatise an L-space (an integration
Riesz space complete w.r.t. the induced distance).
Claudio Sacerdoti Coen [Sun, 5 Nov 2006 17:04:12 +0000 (17:04 +0000)]
Some clean-up here and there in dama (coercions removed, implicits added, etc.)
Claudio Sacerdoti Coen [Sun, 5 Nov 2006 16:31:53 +0000 (16:31 +0000)]
Almost every hand-inserted coercion removed since a bug in the coercion
machinery has been fixed.
Claudio Sacerdoti Coen [Sun, 5 Nov 2006 16:19:38 +0000 (16:19 +0000)]
Bug fixed: the disambiguation domain for a record with left parameters was
not obtained with a pre-visit. The result was that often Failures were detected
later than possible with consequent waste of time.
Claudio Sacerdoti Coen [Sun, 5 Nov 2006 16:14:41 +0000 (16:14 +0000)]
Critical bug finally found after a long chasing!!!
When looking for a coercion over a non meta closed term, often the case was
not detected and a Failure was raised instead of Uncertain.
Claudio Sacerdoti Coen [Sun, 5 Nov 2006 10:14:04 +0000 (10:14 +0000)]
Added more typing information to remove a coercion.
Enrico Zoli [Fri, 3 Nov 2006 16:58:51 +0000 (16:58 +0000)]
Integration f_algebras declassed.
We suppose to prove everything on integration_riesz_spaces.
However, the definition or weak order unit is complex because of the sup
on sequences.
Enrico Zoli [Fri, 3 Nov 2006 14:39:51 +0000 (14:39 +0000)]
Up to absolute value
Stefano Zacchiroli [Fri, 3 Nov 2006 13:46:17 +0000 (13:46 +0000)]
preliminary support for hbugs
added to the cicbrowser the CTRL-l binding for highlighting the URL (a-la-firefox)
Enrico Zoli [Fri, 3 Nov 2006 11:15:03 +0000 (11:15 +0000)]
Up to max (up to a bug).
Enrico Zoli [Tue, 31 Oct 2006 18:23:36 +0000 (18:23 +0000)]
We begin to play the real game: we have defined real numbers and
constructive connectives (only the disjunction for now) and we are
trying to define the max between two real numbers as the limit of a
particular cauchy sequence. Cool.
Enrico Zoli [Tue, 31 Oct 2006 15:38:22 +0000 (15:38 +0000)]
Integration_algebras.ma split into 6 different files.
Enrico Zoli [Tue, 31 Oct 2006 15:36:44 +0000 (15:36 +0000)]
Syntax changed (to be changed back) for left parameters of inductive types.
Claudio Sacerdoti Coen [Tue, 31 Oct 2006 12:33:21 +0000 (12:33 +0000)]
The OK button of the disambiguation errors interface now adds aliases to the
current script. However, the aliases are used only in passes 1 and 3 :-(
Claudio Sacerdoti Coen [Tue, 31 Oct 2006 09:19:19 +0000 (09:19 +0000)]
Bug fixed: inductive types were no longer removed from the environment during
a remove_single_obj.
Claudio Sacerdoti Coen [Tue, 31 Oct 2006 09:03:15 +0000 (09:03 +0000)]
New behaviour of the disambiguation error messages: errors generated without
using coercions are shown only when More is pressed.
Claudio Sacerdoti Coen [Mon, 30 Oct 2006 18:10:25 +0000 (18:10 +0000)]
TermAcicContent.Interpretation_not_found catched and handled correctly.
Claudio Sacerdoti Coen [Mon, 30 Oct 2006 18:03:04 +0000 (18:03 +0000)]
Up to integration f-algebras.
Claudio Sacerdoti Coen [Mon, 30 Oct 2006 17:31:31 +0000 (17:31 +0000)]
Debugging code is now controlled by the debug flag.
Andrea Asperti [Mon, 30 Oct 2006 16:56:28 +0000 (16:56 +0000)]
library = yes!
Claudio Sacerdoti Coen [Mon, 30 Oct 2006 16:40:19 +0000 (16:40 +0000)]
remove_obj is now much faster:
1. the code was utterly messy, trying to remove from the DB files and
to remove from disk #xpointer uris.
2. LIKE substituted by =
3. added QUICK and LOW_PRIORITY to the DELETE statement
4. removed unuseful and unused debugging code that used to slow down every
deletion
Ferruccio Guidi [Sun, 29 Oct 2006 15:11:56 +0000 (15:11 +0000)]
Level-1/LambdaDelta now compiles fine
Claudio Sacerdoti Coen [Sun, 29 Oct 2006 09:32:07 +0000 (09:32 +0000)]
Added target preall.opt.
Claudio Sacerdoti Coen [Sat, 28 Oct 2006 17:12:31 +0000 (17:12 +0000)]
GRAVE BUG IN COERCIONS FIXED: the insertion of a coercion used to introduce
applications of applications (that are forbidden and not handled properly).
Claudio Sacerdoti Coen [Thu, 26 Oct 2006 14:17:06 +0000 (14:17 +0000)]
Better label for the disambiguation errors window.
Claudio Sacerdoti Coen [Thu, 26 Oct 2006 14:15:47 +0000 (14:15 +0000)]
New (and much more complex) disambiguation error interface.
Errors are now categorized according to:
1. location
2. error message
3. environment
Claudio Sacerdoti Coen [Thu, 26 Oct 2006 11:31:22 +0000 (11:31 +0000)]
More timeout added to autos here and there.
Claudio Sacerdoti Coen [Wed, 25 Oct 2006 17:42:45 +0000 (17:42 +0000)]
1. is_meta_closed should be applied only to terms on which a substitution
has already been applied. Fixed here and there.
Note: it is not possible to add a subst parameter to is_meta_closed since
the function is declared in cic/CicUtil and it is used where the unification
is not available (e.g. in whelp and library)
2. known (but never verified before) bug fixed: delifting should fail
(instead of raising Uncertain) iff the local context is not meta_closed.
The test used to be "does not contain a Meta"
Ferruccio Guidi [Wed, 25 Oct 2006 16:47:18 +0000 (16:47 +0000)]
till some patches
Ferruccio Guidi [Wed, 25 Oct 2006 14:25:14 +0000 (14:25 +0000)]
the incomplete proofs were axiomatized
Ferruccio Guidi [Wed, 25 Oct 2006 14:12:08 +0000 (14:12 +0000)]
some patches. still does not compile properly
Claudio Sacerdoti Coen [Wed, 25 Oct 2006 12:51:56 +0000 (12:51 +0000)]
Added timeouts to auto here and there.
Claudio Sacerdoti Coen [Wed, 25 Oct 2006 12:44:25 +0000 (12:44 +0000)]
Added timeout to autos here and there.
Claudio Sacerdoti Coen [Wed, 25 Oct 2006 12:41:21 +0000 (12:41 +0000)]
1. bug fixed: Unicode characters that are not mapped to TeX macros used to
be post-fixed with a blank
2. bug fixed: the textual pretty-printer does not implement the same
spacing politics of GtkMathView. Since that politics is very very complex
to implement, I try a different solution: we explicitly insert a space
where we want one. The widget does not seem to be disturbed by this.
This way the let ... rec and match ... with constructs are now printed
correctly and they can be read back.
3. syntax change: applicative patterns no longer require parentheses around
them
Claudio Sacerdoti Coen [Wed, 25 Oct 2006 12:33:38 +0000 (12:33 +0000)]
/home/fguidi/... => ../../...
Ferruccio Guidi [Wed, 25 Oct 2006 12:26:16 +0000 (12:26 +0000)]
we removed about 100 match-with costruction turning them into applications
Andrea Asperti [Wed, 25 Oct 2006 09:41:45 +0000 (09:41 +0000)]
Added a couple of flags to auto
Claudio Sacerdoti Coen [Wed, 25 Oct 2006 09:31:58 +0000 (09:31 +0000)]
Our unification used to guess a very complex argument of an apply in
fermat_little_theorem. It does no longer, but the old behaviour seems to be
really lucky. Thus I change the .ma file.
Claudio Sacerdoti Coen [Wed, 25 Oct 2006 09:28:11 +0000 (09:28 +0000)]
Two lemmas that used to pass no more now pass again. Bug simply because every
tactic argument now requires less question marks :-(
Enrico Zoli [Tue, 24 Oct 2006 16:52:08 +0000 (16:52 +0000)]
Added unit to rings.
Enrico Zoli [Tue, 24 Oct 2006 16:03:12 +0000 (16:03 +0000)]
More coercions added in the algebraic hierarchy.
Enrico Zoli [Tue, 24 Oct 2006 14:10:08 +0000 (14:10 +0000)]
Up to f_algebras.
Enrico Tassi [Tue, 24 Oct 2006 08:02:35 +0000 (08:02 +0000)]
fixed the ugly button added by csc, now it is inside a buttonbar and uses the default gnome stop icon.
Enrico Tassi [Tue, 24 Oct 2006 08:02:02 +0000 (08:02 +0000)]
removed equality_retrieval
Claudio Sacerdoti Coen [Mon, 23 Oct 2006 22:20:16 +0000 (22:20 +0000)]
Better (and more localized) error message for sort_of_prod.
Claudio Sacerdoti Coen [Mon, 23 Oct 2006 20:23:24 +0000 (20:23 +0000)]
CicUniv.UniverseInconsistency is no handled correcly.
Claudio Sacerdoti Coen [Mon, 23 Oct 2006 13:22:25 +0000 (13:22 +0000)]
binaries/saturate no longer compiled since it does not compile any longer after
the huge refactoring of auto/paramodulation by Andrea
Andrea Asperti [Fri, 20 Oct 2006 15:44:48 +0000 (15:44 +0000)]
Demodulate and applyS moved form saturation to auto.
Andrea Asperti [Fri, 20 Oct 2006 15:43:02 +0000 (15:43 +0000)]
Major changes to auto, documented on the helm mailing list.
projects / helm.git / log