]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agoAvoid translating back recursive fixes to the same URI.
Claudio Sacerdoti Coen [Thu, 21 Feb 2008 19:02:04 +0000 (19:02 +0000)]
Avoid translating back recursive fixes to the same URI.

16 years agoAvoid application to 0 arguments.
Claudio Sacerdoti Coen [Thu, 21 Feb 2008 18:57:28 +0000 (18:57 +0000)]
Avoid application to 0 arguments.

16 years agoBetter handling of exceptions.
Claudio Sacerdoti Coen [Thu, 21 Feb 2008 18:56:44 +0000 (18:56 +0000)]
Better handling of exceptions.

16 years agosvn:ignores fixed
Ferruccio Guidi [Thu, 21 Feb 2008 15:32:50 +0000 (15:32 +0000)]
svn:ignores fixed

16 years ago-onepass option removed from Makefile to comile Base-2/ext/arith.ma ???
Ferruccio Guidi [Wed, 20 Feb 2008 19:30:11 +0000 (19:30 +0000)]
-onepass option removed from Makefile to comile Base-2/ext/arith.ma ???

16 years agoLambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES
Ferruccio Guidi [Wed, 20 Feb 2008 18:53:47 +0000 (18:53 +0000)]
LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES
some additions and redundant dependences fixed

16 years agosplat_args is now better understood and debugged: we need TWO splat_args, one when
Enrico Tassi [Wed, 20 Feb 2008 17:48:16 +0000 (17:48 +0000)]
splat_args is now better understood and debugged: we need TWO splat_args, one when
the term is a Rel (that skips the bound variables) and one when the term is a Fix
(that passes bound variables around).

16 years agoadded small test, fixed some bugs
Enrico Tassi [Wed, 20 Feb 2008 16:53:59 +0000 (16:53 +0000)]
added small test, fixed some bugs

16 years agomany fixed in translation functions
Enrico Tassi [Wed, 20 Feb 2008 14:49:22 +0000 (14:49 +0000)]
many fixed in translation functions

16 years agodependences needed a fix :)
Ferruccio Guidi [Tue, 19 Feb 2008 19:24:14 +0000 (19:24 +0000)]
dependences needed a fix :)

16 years agowe are moving the devel root one dir level up
Ferruccio Guidi [Tue, 19 Feb 2008 17:16:12 +0000 (17:16 +0000)]
we are moving the devel root one dir level up

16 years ago...
Enrico Tassi [Tue, 19 Feb 2008 17:05:43 +0000 (17:05 +0000)]
...

16 years agosnapshot inverse tranformation
Enrico Tassi [Tue, 19 Feb 2008 16:55:40 +0000 (16:55 +0000)]
snapshot inverse tranformation

16 years agotransformation almost finisced, not tested
Enrico Tassi [Tue, 19 Feb 2008 15:38:00 +0000 (15:38 +0000)]
transformation almost finisced, not tested

16 years agonow inline "file.ma" is allowed.
Ferruccio Guidi [Tue, 19 Feb 2008 13:00:29 +0000 (13:00 +0000)]
now inline "file.ma" is allowed.
file.ma must be compiled and all its contents are inlined

16 years agoAdded o.ma (some results about the magnitude of functions *)
Andrea Asperti [Tue, 19 Feb 2008 12:27:10 +0000 (12:27 +0000)]
Added o.ma (some results about the magnitude of functions *)

16 years agoinitial steps of convertibility
Enrico Tassi [Tue, 19 Feb 2008 11:13:39 +0000 (11:13 +0000)]
initial steps of convertibility

16 years agosome bits of reduction, reusing psubst
Enrico Tassi [Mon, 18 Feb 2008 16:31:32 +0000 (16:31 +0000)]
some bits of reduction, reusing psubst

16 years agoComplete proof of Bertrand for n >= 256.
Andrea Asperti [Mon, 18 Feb 2008 08:56:40 +0000 (08:56 +0000)]
Complete proof of Bertrand for n >= 256.
Removed the baseuri form all files in nat.

16 years agoPrima versione di bertrand. Tanti cambiamenti qua e la.
Andrea Asperti [Thu, 14 Feb 2008 15:41:46 +0000 (15:41 +0000)]
Prima versione di bertrand. Tanti cambiamenti qua e la.

16 years agobaseuris removed from files
Ferruccio Guidi [Wed, 13 Feb 2008 17:56:43 +0000 (17:56 +0000)]
baseuris removed from files

16 years agofixed dependences
Ferruccio Guidi [Wed, 13 Feb 2008 17:24:39 +0000 (17:24 +0000)]
fixed dependences

16 years agoconversion half inplemented
Enrico Tassi [Wed, 13 Feb 2008 17:18:25 +0000 (17:18 +0000)]
conversion half inplemented

16 years agorenaming
Ferruccio Guidi [Wed, 13 Feb 2008 17:15:06 +0000 (17:15 +0000)]
renaming

16 years agoreordered cases
Enrico Tassi [Wed, 13 Feb 2008 16:00:16 +0000 (16:00 +0000)]
reordered cases

16 years agoreorganization of sources
Enrico Tassi [Wed, 13 Feb 2008 15:42:28 +0000 (15:42 +0000)]
reorganization of sources

16 years agosubstituion and lifting implemented
Enrico Tassi [Wed, 13 Feb 2008 15:35:43 +0000 (15:35 +0000)]
substituion and lifting implemented

16 years agorenaming
Ferruccio Guidi [Wed, 13 Feb 2008 13:40:54 +0000 (13:40 +0000)]
renaming

16 years agofactorized common components of objects
Enrico Tassi [Wed, 13 Feb 2008 13:17:38 +0000 (13:17 +0000)]
factorized common components of objects

16 years agoadded Local pragma, moved leftno and inductive into obj, added relevance attribute...
Enrico Tassi [Wed, 13 Feb 2008 13:01:15 +0000 (13:01 +0000)]
added Local pragma, moved leftno and inductive into obj, added relevance attribute of parameters

16 years agoadded leftno to indtypes, better indentation and comments
Enrico Tassi [Wed, 13 Feb 2008 12:46:12 +0000 (12:46 +0000)]
added leftno to indtypes, better indentation and comments

16 years agonCic almost finished
Enrico Tassi [Tue, 12 Feb 2008 18:02:14 +0000 (18:02 +0000)]
nCic almost finished

16 years agorenaming
Ferruccio Guidi [Tue, 12 Feb 2008 16:21:19 +0000 (16:21 +0000)]
renaming

16 years agoregeneration with new results
Ferruccio Guidi [Tue, 12 Feb 2008 16:02:28 +0000 (16:02 +0000)]
regeneration with new results

16 years agofixed path for matitadep
Enrico Tassi [Tue, 12 Feb 2008 12:09:41 +0000 (12:09 +0000)]
fixed path for matitadep

16 years agofixed make dist
Enrico Tassi [Tue, 12 Feb 2008 12:09:20 +0000 (12:09 +0000)]
fixed make dist

16 years agobetter error message in case inclusion failed
Enrico Tassi [Tue, 12 Feb 2008 12:08:39 +0000 (12:08 +0000)]
better error message in case inclusion failed

16 years agoallow to use "../foo/bar.ma" as a path for the include statement
Enrico Tassi [Tue, 12 Feb 2008 12:06:26 +0000 (12:06 +0000)]
allow to use "../foo/bar.ma" as a path for the include statement

16 years agoprogress.
Andrea Asperti [Fri, 8 Feb 2008 17:04:43 +0000 (17:04 +0000)]
progress.

16 years agoA formalization of modified realisability with truth as in
Claudio Sacerdoti Coen [Fri, 8 Feb 2008 15:22:32 +0000 (15:22 +0000)]
A formalization of modified realisability with truth as in
``Internalising modified realisability in constructive type theory'',
Erik Palmgren, Logical Methods in Computer Science, Vol 1. (2:2), 2005, pp 1--7.

16 years agoBug fixed in generation of elimination principles of inductive types having
Claudio Sacerdoti Coen [Fri, 8 Feb 2008 13:44:54 +0000 (13:44 +0000)]
Bug fixed in generation of elimination principles of inductive types having
at least one constructor of type (A -> i) -> i that was not the last
constructor.

16 years agoprodT merged with prod
Claudio Sacerdoti Coen [Fri, 8 Feb 2008 11:50:42 +0000 (11:50 +0000)]
prodT merged with prod
fstT merged with fst
sndT merged with fst

16 years agoProdT was a perfect copy of Prod. Removed.
Claudio Sacerdoti Coen [Thu, 7 Feb 2008 18:08:50 +0000 (18:08 +0000)]
ProdT was a perfect copy of Prod. Removed.
Sum is now in Type.

16 years agoResults about Chebyshev teta function.
Andrea Asperti [Thu, 7 Feb 2008 12:02:01 +0000 (12:02 +0000)]
Results about Chebyshev teta function.

16 years agocic defined (half)
Enrico Tassi [Tue, 5 Feb 2008 17:45:38 +0000 (17:45 +0000)]
cic defined (half)

16 years agoSome more theorems.
Andrea Asperti [Tue, 5 Feb 2008 16:21:37 +0000 (16:21 +0000)]
Some more theorems.

16 years agoreindent
Enrico Tassi [Tue, 5 Feb 2008 16:12:33 +0000 (16:12 +0000)]
reindent

16 years agooldenv2newenv cache
Enrico Tassi [Tue, 5 Feb 2008 16:06:20 +0000 (16:06 +0000)]
oldenv2newenv cache

16 years agouri and references(uri)
Enrico Tassi [Tue, 5 Feb 2008 15:54:52 +0000 (15:54 +0000)]
uri and references(uri)

16 years agouri -> reference (2)
Enrico Tassi [Tue, 5 Feb 2008 15:23:08 +0000 (15:23 +0000)]
uri -> reference (2)

16 years agouri -> reference
Enrico Tassi [Tue, 5 Feb 2008 15:20:38 +0000 (15:20 +0000)]
uri -> reference

16 years agolower bound for neper's constant
Wilmer Ricciotti [Tue, 5 Feb 2008 15:10:20 +0000 (15:10 +0000)]
lower bound for neper's constant

16 years agosad snapshot
Enrico Tassi [Mon, 4 Feb 2008 15:13:59 +0000 (15:13 +0000)]
sad snapshot

16 years agosnapshot
Enrico Tassi [Mon, 4 Feb 2008 11:00:54 +0000 (11:00 +0000)]
snapshot

16 years agosnapshot
Enrico Tassi [Mon, 4 Feb 2008 10:57:45 +0000 (10:57 +0000)]
snapshot

16 years agoImproved approximations for A and prim.
Andrea Asperti [Mon, 4 Feb 2008 08:55:10 +0000 (08:55 +0000)]
Improved approximations for A and prim.

16 years agoSome improvement.
Andrea Asperti [Mon, 4 Feb 2008 08:39:17 +0000 (08:39 +0000)]
Some improvement.

16 years agovery bad bug found, asert false in cicReduction when a clear is performed
Enrico Tassi [Fri, 1 Feb 2008 09:29:09 +0000 (09:29 +0000)]
very bad bug found, asert false in cicReduction when a clear is performed

16 years agoOne Obj.magic implemented, trust changed to false.
Wilmer Ricciotti [Thu, 31 Jan 2008 16:30:40 +0000 (16:30 +0000)]
One Obj.magic implemented, trust changed to false.

16 years agoTransformation back and forth between old and new representation
Wilmer Ricciotti [Thu, 31 Jan 2008 16:20:46 +0000 (16:20 +0000)]
Transformation back and forth between old and new representation

16 years agosnapshot
Enrico Tassi [Thu, 31 Jan 2008 15:27:47 +0000 (15:27 +0000)]
snapshot

16 years agonew uri defined
Enrico Tassi [Thu, 31 Jan 2008 15:06:31 +0000 (15:06 +0000)]
new uri defined

16 years agoSquare root added.
Wilmer Ricciotti [Thu, 31 Jan 2008 14:51:45 +0000 (14:51 +0000)]
Square root added.

16 years agosnapshot]
Enrico Tassi [Thu, 31 Jan 2008 14:50:19 +0000 (14:50 +0000)]
snapshot]

16 years agosnapshot
Enrico Tassi [Thu, 31 Jan 2008 12:43:37 +0000 (12:43 +0000)]
snapshot

16 years agoadded meta for the new kernel
Enrico Tassi [Wed, 30 Jan 2008 16:29:04 +0000 (16:29 +0000)]
added meta for the new kernel

16 years agostub functions to make all compile
Enrico Tassi [Wed, 30 Jan 2008 16:26:06 +0000 (16:26 +0000)]
stub functions to make all compile

16 years agobasic organization of the new kernel
Enrico Tassi [Wed, 30 Jan 2008 10:42:22 +0000 (10:42 +0000)]
basic organization of the new kernel

16 years agoImproved approximations
Andrea Asperti [Wed, 30 Jan 2008 09:13:06 +0000 (09:13 +0000)]
Improved approximations

16 years agoNew approximtions.
Andrea Asperti [Tue, 29 Jan 2008 10:57:02 +0000 (10:57 +0000)]
New approximtions.

16 years ago...
Enrico Tassi [Thu, 24 Jan 2008 10:37:11 +0000 (10:37 +0000)]
...

16 years agosnapshot with more duality, almost where we left without duality
Enrico Tassi [Wed, 23 Jan 2008 12:44:39 +0000 (12:44 +0000)]
snapshot with more duality, almost where we left without duality

16 years ago...
Enrico Tassi [Tue, 22 Jan 2008 17:54:05 +0000 (17:54 +0000)]
...

16 years agoBertrand's conjecture (weak), some work in progress
Wilmer Ricciotti [Tue, 22 Jan 2008 10:41:43 +0000 (10:41 +0000)]
Bertrand's conjecture (weak), some work in progress

16 years agosnapshot
Enrico Tassi [Mon, 21 Jan 2008 18:05:11 +0000 (18:05 +0000)]
snapshot

16 years agoMatitac now accepts multiple targets :-) (but only in the same root :-(
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:35:11 +0000 (17:35 +0000)]
Matitac now accepts multiple targets :-) (but only in the same root :-(

16 years agoHack for code extraction re-linked, but disactivated.
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:30:35 +0000 (17:30 +0000)]
Hack for code extraction re-linked, but disactivated.

16 years agoOld tiny freescale experiment get rid of.
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:29:48 +0000 (17:29 +0000)]
Old tiny freescale experiment get rid of.
New shiny freescale formalization by Cosimo Oliboni <oliboni@cs.unibo.it>,
described in his Laurea Thesis.

16 years agoTypo fixed.
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:18:32 +0000 (17:18 +0000)]
Typo fixed.

16 years agosnopshot before isabellization
Enrico Tassi [Mon, 21 Jan 2008 11:21:36 +0000 (11:21 +0000)]
snopshot before isabellization

16 years agosnapshot
Enrico Tassi [Wed, 16 Jan 2008 15:48:53 +0000 (15:48 +0000)]
snapshot

16 years ago3.27 ok
Enrico Tassi [Wed, 16 Jan 2008 13:32:05 +0000 (13:32 +0000)]
3.27 ok

16 years agoyes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!
Enrico Tassi [Wed, 16 Jan 2008 12:04:06 +0000 (12:04 +0000)]
yes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!

16 years agoupdate: upper bound for prim
Wilmer Ricciotti [Tue, 15 Jan 2008 14:38:50 +0000 (14:38 +0000)]
update: upper bound for prim

16 years agomore lemmas, til 3.26
Enrico Tassi [Mon, 14 Jan 2008 17:02:46 +0000 (17:02 +0000)]
more lemmas, til 3.26

16 years agonew deps
Enrico Tassi [Mon, 14 Jan 2008 16:37:39 +0000 (16:37 +0000)]
new deps

16 years agofirst lemma
Enrico Tassi [Mon, 14 Jan 2008 15:20:51 +0000 (15:20 +0000)]
first lemma

16 years agofixed a pulback and proved 3.17
Enrico Tassi [Mon, 14 Jan 2008 14:58:26 +0000 (14:58 +0000)]
fixed a pulback and proved 3.17

16 years agoadded some doc
Enrico Tassi [Mon, 14 Jan 2008 10:05:45 +0000 (10:05 +0000)]
added some doc

16 years agouser time is now printed correctly
Enrico Tassi [Mon, 14 Jan 2008 09:03:13 +0000 (09:03 +0000)]
user time is now printed correctly

16 years agobetter parsing of the root file
Enrico Tassi [Mon, 14 Jan 2008 09:03:01 +0000 (09:03 +0000)]
better parsing of the root file

16 years agofixed uris
Enrico Tassi [Mon, 14 Jan 2008 09:02:41 +0000 (09:02 +0000)]
fixed uris

16 years agoChebyshev's upper bound on prim
Wilmer Ricciotti [Mon, 14 Jan 2008 07:43:37 +0000 (07:43 +0000)]
Chebyshev's upper bound on prim

16 years agoremoved path for contribs
Enrico Tassi [Fri, 11 Jan 2008 19:13:29 +0000 (19:13 +0000)]
removed path for contribs

16 years agoadded a warning when a file is not compiled cause its buri is readonly
Enrico Tassi [Fri, 11 Jan 2008 19:11:09 +0000 (19:11 +0000)]
added a warning when a file is not compiled cause its buri is readonly

16 years agoMake does not even try to build files that would be compiled in read-only
Enrico Tassi [Fri, 11 Jan 2008 19:05:05 +0000 (19:05 +0000)]
Make does not even try to build files that would be compiled in read-only
baseuris

16 years agoI'll talk again with ferruccio, for the moment this is the right
Enrico Tassi [Fri, 11 Jan 2008 16:13:49 +0000 (16:13 +0000)]
I'll talk again with ferruccio, for the moment this is the right
way to allow every user that does and svn co to compile everithing.

16 years agoanother fix to make it more resistant
Enrico Tassi [Fri, 11 Jan 2008 15:52:06 +0000 (15:52 +0000)]
another fix to make it more resistant

16 years agomany sed to use notation for rewriting
Enrico Tassi [Fri, 11 Jan 2008 15:37:11 +0000 (15:37 +0000)]
many sed to use notation for rewriting

16 years ago.opt before .byte
Enrico Tassi [Fri, 11 Jan 2008 15:16:10 +0000 (15:16 +0000)]
.opt before .byte