]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agoAdded summation formula for the power of a binomial.
Wilmer Ricciotti [Sun, 9 Dec 2007 23:28:01 +0000 (23:28 +0000)]
Added summation formula for the power of a binomial.

16 years agothe is_structure is a bad idea if you don't have canonical structures.
Enrico Tassi [Sat, 8 Dec 2007 10:36:00 +0000 (10:36 +0000)]
the is_structure is a bad idea if you don't have canonical structures.

16 years agoBinomial coefficients and costant e.
Andrea Asperti [Fri, 7 Dec 2007 11:41:49 +0000 (11:41 +0000)]
Binomial coefficients and costant e.

16 years agoA few more theorems.
Andrea Asperti [Fri, 7 Dec 2007 11:38:57 +0000 (11:38 +0000)]
A few more theorems.

16 years agodump spurious errors max
Stefano Zacchiroli [Thu, 6 Dec 2007 15:29:52 +0000 (15:29 +0000)]
dump spurious errors max

16 years agoexcede->excess
Enrico Tassi [Thu, 6 Dec 2007 11:17:39 +0000 (11:17 +0000)]
excede->excess

16 years agoexcedence -> excess
Enrico Tassi [Thu, 6 Dec 2007 10:16:17 +0000 (10:16 +0000)]
excedence -> excess

16 years agoweight -> value
Enrico Tassi [Thu, 6 Dec 2007 09:57:03 +0000 (09:57 +0000)]
weight -> value

16 years agodump result table in \TeX format
Stefano Zacchiroli [Wed, 5 Dec 2007 15:26:53 +0000 (15:26 +0000)]
dump result table in \TeX format

16 years ago...
Claudio Sacerdoti Coen [Wed, 5 Dec 2007 13:47:20 +0000 (13:47 +0000)]
...

16 years agoRepeated errors are not duplicated.
Claudio Sacerdoti Coen [Tue, 4 Dec 2007 22:08:45 +0000 (22:08 +0000)]
Repeated errors are not duplicated.

16 years agoEven if the error is not localized, it was not a good idea to make the unification...
Claudio Sacerdoti Coen [Tue, 4 Dec 2007 22:01:38 +0000 (22:01 +0000)]
Even if the error is not localized, it was not a good idea to make the unification error
escape.

16 years agorefactoring of some lemmas, shorter proofs
Enrico Tassi [Tue, 4 Dec 2007 18:40:03 +0000 (18:40 +0000)]
refactoring of some lemmas, shorter proofs

16 years agoSome terms are not localized from the very beginning :-(
Claudio Sacerdoti Coen [Tue, 4 Dec 2007 17:51:09 +0000 (17:51 +0000)]
Some terms are not localized from the very beginning :-(

16 years agoAdded debugging option to ask for all disambiguation errors (even spurious ones)...
Claudio Sacerdoti Coen [Tue, 4 Dec 2007 17:17:04 +0000 (17:17 +0000)]
Added debugging option to ask for all disambiguation errors (even spurious ones) in all passes.

16 years agoOne more error localized. But the code is really ugly here :-(
Claudio Sacerdoti Coen [Tue, 4 Dec 2007 15:56:03 +0000 (15:56 +0000)]
One more error localized. But the code is really ugly here :-(

16 years agoadded do_heavy_checks documentation
Enrico Tassi [Tue, 4 Dec 2007 15:17:01 +0000 (15:17 +0000)]
added do_heavy_checks documentation

16 years agodo_heavy_checks not always true, take ths option from the registry instead
Enrico Tassi [Tue, 4 Dec 2007 15:16:25 +0000 (15:16 +0000)]
do_heavy_checks not always true, take ths option from the registry instead

16 years agoadded do_heavy_checks default
Enrico Tassi [Tue, 4 Dec 2007 15:15:47 +0000 (15:15 +0000)]
added do_heavy_checks default

16 years agoif parameter type is given, this assert is false
Enrico Tassi [Tue, 4 Dec 2007 15:13:43 +0000 (15:13 +0000)]
if parameter type is given, this assert is false

16 years agoOnly errors from passes 4 and 6 are kept.
Claudio Sacerdoti Coen [Tue, 4 Dec 2007 14:12:14 +0000 (14:12 +0000)]
Only errors from passes 4 and 6 are kept.

16 years agoReindented.
Claudio Sacerdoti Coen [Tue, 4 Dec 2007 11:02:16 +0000 (11:02 +0000)]
Reindented.

16 years agosandwitch theorem done
Enrico Tassi [Tue, 4 Dec 2007 09:55:44 +0000 (09:55 +0000)]
sandwitch theorem done

16 years agoremoved all the axioms!!!
Enrico Tassi [Tue, 4 Dec 2007 00:05:46 +0000 (00:05 +0000)]
removed all the axioms!!!

16 years agosligtly more general results, still to reorganize
Enrico Tassi [Tue, 4 Dec 2007 00:01:44 +0000 (00:01 +0000)]
sligtly more general results, still to reorganize

16 years agook
Enrico Tassi [Mon, 3 Dec 2007 23:44:35 +0000 (23:44 +0000)]
ok

16 years ago1 lemma left!!!!
Enrico Tassi [Mon, 3 Dec 2007 15:21:39 +0000 (15:21 +0000)]
1 lemma left!!!!

16 years agoSome progress.
Andrea Asperti [Mon, 3 Dec 2007 11:39:09 +0000 (11:39 +0000)]
Some progress.

16 years agoForward compatibility with new lablgtk2.
Claudio Sacerdoti Coen [Sun, 2 Dec 2007 15:07:05 +0000 (15:07 +0000)]
Forward compatibility with new lablgtk2.

16 years agocarabinieri almost done
Enrico Tassi [Sat, 1 Dec 2007 12:46:08 +0000 (12:46 +0000)]
carabinieri almost done

16 years agocarabinieri almost done
Enrico Tassi [Fri, 30 Nov 2007 17:57:32 +0000 (17:57 +0000)]
carabinieri almost done

16 years agocleanup of the eq_trans burdain
Enrico Tassi [Fri, 30 Nov 2007 14:35:21 +0000 (14:35 +0000)]
cleanup of the eq_trans burdain

16 years ago3.11 !!!
Enrico Tassi [Fri, 30 Nov 2007 12:40:56 +0000 (12:40 +0000)]
3.11 !!!

16 years agoadded a way to generate all the utf8 symbols
Enrico Tassi [Fri, 30 Nov 2007 09:07:40 +0000 (09:07 +0000)]
added a way to generate all the utf8 symbols

16 years agoDead code removed.
Claudio Sacerdoti Coen [Wed, 28 Nov 2007 22:29:16 +0000 (22:29 +0000)]
Dead code removed.

16 years agoBug fixed: an unification exception used to escape during eat_prods.
Claudio Sacerdoti Coen [Wed, 28 Nov 2007 21:08:18 +0000 (21:08 +0000)]
Bug fixed: an unification exception used to escape during eat_prods.

16 years agomore stuff
Enrico Tassi [Wed, 28 Nov 2007 18:12:33 +0000 (18:12 +0000)]
more stuff

16 years ago...
Enrico Tassi [Wed, 28 Nov 2007 17:00:44 +0000 (17:00 +0000)]
...

16 years agoOutput is now in UTF8 character counts.
Claudio Sacerdoti Coen [Tue, 27 Nov 2007 17:44:11 +0000 (17:44 +0000)]
Output is now in UTF8 character counts.

16 years agoOptions declared but not parsed.
Claudio Sacerdoti Coen [Tue, 27 Nov 2007 17:14:52 +0000 (17:14 +0000)]
Options declared but not parsed.

16 years agoPorted to camlp5 < 5.00
Claudio Sacerdoti Coen [Tue, 27 Nov 2007 17:07:08 +0000 (17:07 +0000)]
Ported to camlp5 < 5.00

16 years agoBack-ported to camlp5 < 5.00.
Claudio Sacerdoti Coen [Tue, 27 Nov 2007 16:56:54 +0000 (16:56 +0000)]
Back-ported to camlp5 < 5.00.

16 years ago....
Enrico Tassi [Tue, 27 Nov 2007 16:44:49 +0000 (16:44 +0000)]
....

16 years ago...
Enrico Tassi [Tue, 27 Nov 2007 16:44:11 +0000 (16:44 +0000)]
...

16 years agoremove debug fake data
Stefano Zacchiroli [Tue, 27 Nov 2007 16:23:21 +0000 (16:23 +0000)]
remove debug fake data

16 years ago(hackish) scripts for testing spurious disambiguation error criteria
Stefano Zacchiroli [Tue, 27 Nov 2007 16:22:45 +0000 (16:22 +0000)]
(hackish) scripts for testing spurious disambiguation error criteria

16 years agoadd "-order" cmdline option to just print a possible build order of the given *.ma...
Stefano Zacchiroli [Tue, 27 Nov 2007 15:15:20 +0000 (15:15 +0000)]
add "-order" cmdline option to just print a possible build order of the given *.ma files and then quit

16 years agochange naming scheme for rottened script, so that they do not mess up matitadep/make...
Stefano Zacchiroli [Tue, 27 Nov 2007 15:13:38 +0000 (15:13 +0000)]
change naming scheme for rottened script, so that they do not mess up matitadep/make assumptions

16 years ago...
Enrico Tassi [Tue, 27 Nov 2007 12:33:14 +0000 (12:33 +0000)]
...

16 years agomajor reorganization (read cleanup)
Enrico Tassi [Tue, 27 Nov 2007 11:56:08 +0000 (11:56 +0000)]
major reorganization (read cleanup)

16 years agobir georganization, most of the structures done
Enrico Tassi [Tue, 27 Nov 2007 11:36:52 +0000 (11:36 +0000)]
bir georganization, most of the structures done

16 years agoavoid rottening of constructor names in pattern matchings
Stefano Zacchiroli [Tue, 27 Nov 2007 11:19:14 +0000 (11:19 +0000)]
avoid rottening of constructor names in pattern matchings

16 years agoignore sqlite db and rottener* executables
Stefano Zacchiroli [Tue, 27 Nov 2007 09:28:59 +0000 (09:28 +0000)]
ignore sqlite db and rottener* executables

16 years ago- use "O" as the rottening token
Stefano Zacchiroli [Tue, 27 Nov 2007 09:27:01 +0000 (09:27 +0000)]
- use "O" as the rottening token
- add generation of a trailer with error location information

16 years agomake target for cleaning rottened files
Stefano Zacchiroli [Tue, 27 Nov 2007 09:26:34 +0000 (09:26 +0000)]
make target for cleaning rottened files

16 years agoreorganization of many files according to the new basic picture.
Enrico Tassi [Mon, 26 Nov 2007 16:54:32 +0000 (16:54 +0000)]
reorganization of many files according to the new basic picture.
todo: premetric lattice and the various coercions

16 years agofirst draft of a script to mechanically introduce (disambiguation) errors into Matita...
Stefano Zacchiroli [Mon, 26 Nov 2007 16:23:50 +0000 (16:23 +0000)]
first draft of a script to mechanically introduce (disambiguation) errors into Matita scripts

16 years agoignore *.o
Stefano Zacchiroli [Mon, 26 Nov 2007 15:31:10 +0000 (15:31 +0000)]
ignore *.o

16 years agoadd dump of position information in the lexed file
Stefano Zacchiroli [Mon, 26 Nov 2007 15:30:52 +0000 (15:30 +0000)]
add dump of position information in the lexed file

16 years agoAxiom moved from ex_deriv to deriv where it belongs to.
Claudio Sacerdoti Coen [Mon, 26 Nov 2007 12:43:17 +0000 (12:43 +0000)]
Axiom moved from ex_deriv to deriv where it belongs to.

16 years agoNotation improved.
Claudio Sacerdoti Coen [Mon, 26 Nov 2007 12:42:51 +0000 (12:42 +0000)]
Notation improved.

16 years agoSome code clean-up.
Claudio Sacerdoti Coen [Mon, 26 Nov 2007 12:06:29 +0000 (12:06 +0000)]
Some code clean-up.

16 years agoDisambiguation error compaction is now performed in the same way by matita and
Claudio Sacerdoti Coen [Mon, 26 Nov 2007 11:54:52 +0000 (11:54 +0000)]
Disambiguation error compaction is now performed in the same way by matita and
matitac. The difference is that matitac shows every error in every pass,
marking spurious errors as spurious.

16 years agofor csc
Enrico Tassi [Mon, 26 Nov 2007 10:55:46 +0000 (10:55 +0000)]
for csc

16 years agopretty
Enrico Tassi [Mon, 26 Nov 2007 10:52:53 +0000 (10:52 +0000)]
pretty

16 years agoPatch to automatically generate filename.error.md5.ma scripts every time a
Claudio Sacerdoti Coen [Mon, 26 Nov 2007 10:22:36 +0000 (10:22 +0000)]
Patch to automatically generate filename.error.md5.ma scripts every time a
disambiguation error is faced by the user.

16 years agoAlmost there.
Andrea Asperti [Mon, 26 Nov 2007 08:45:42 +0000 (08:45 +0000)]
Almost there.

16 years agoThis version of disambiguate.ml implements yet another (better?) criterio for
Claudio Sacerdoti Coen [Sun, 25 Nov 2007 11:13:48 +0000 (11:13 +0000)]
This version of disambiguate.ml implements yet another (better?) criterio for
spurious error detection. An error is spurious iff:

a) it is obtained interpreting a symbol s using an interpretation \phi
b) there exists another interpretation \phi' such that
   1) dom(\phi') = dom(\phi)
   2) \phi' is valid

It should be true that no nested error locations should occur.
In principle this also suggests the possibility of changing the user interface
to show all alternative errors at the same time.

16 years agoBug fixed: an unification exception used to escape when coercions were disabled.
Claudio Sacerdoti Coen [Sun, 25 Nov 2007 10:44:38 +0000 (10:44 +0000)]
Bug fixed: an unification exception used to escape when coercions were disabled.

16 years agosince the previous commit fixed some bugs when the context has a deleted hp,
Enrico Tassi [Fri, 23 Nov 2007 18:15:10 +0000 (18:15 +0000)]
since the previous commit fixed some bugs when the context has a deleted hp,
the script is better

16 years agorestored the right context used to generate names. see the comment
Enrico Tassi [Fri, 23 Nov 2007 17:59:19 +0000 (17:59 +0000)]
restored the right context used to generate names. see the comment

16 years agoThis alternative version of disambiguate.crit2 implements the following
Claudio Sacerdoti Coen [Fri, 23 Nov 2007 15:59:43 +0000 (15:59 +0000)]
This alternative version of disambiguate.crit2 implements the following
criterion for spurious error detection:

an error is spurious iff:
  a) it is obtained interpreting the symbol s with the interpretation \phi
  b) there exists another interpretation \phi' such that
     1) dom(\phi) = dom(\phi')
     2) \phi' is valid
     3) \phi(x)=\phi'(x) for each x != s

More (but not too many) errors are spurious according to this criterion.

16 years agofast and sound registry lists
Enrico Tassi [Fri, 23 Nov 2007 15:26:03 +0000 (15:26 +0000)]
fast and sound registry lists
faster matitamake setup

16 years ago* NOT RELEASED YET
Stefano Zacchiroli [Fri, 23 Nov 2007 13:25:21 +0000 (13:25 +0000)]
* NOT RELEASED YET

16 years ago* bump deps on lablgtk2 to match lates upstream
Stefano Zacchiroli [Fri, 23 Nov 2007 13:00:08 +0000 (13:00 +0000)]
* bump deps on lablgtk2 to match lates upstream
* debian/control
  - fix VCS field names (now supported natively by dpkg)
  - add Homepage field

16 years agolemma finisced
Enrico Tassi [Thu, 22 Nov 2007 16:58:04 +0000 (16:58 +0000)]
lemma finisced

16 years agoBug fixed in printing of passes in error messages.
Claudio Sacerdoti Coen [Thu, 22 Nov 2007 16:37:43 +0000 (16:37 +0000)]
Bug fixed in printing of passes in error messages.

16 years agolemma 3.57 half done!!!!
Enrico Tassi [Thu, 22 Nov 2007 16:20:50 +0000 (16:20 +0000)]
lemma 3.57 half done!!!!

16 years agonotation in autogui
Enrico Tassi [Thu, 22 Nov 2007 14:32:30 +0000 (14:32 +0000)]
notation in autogui

16 years agoBig progress
Andrea Asperti [Thu, 22 Nov 2007 14:25:36 +0000 (14:25 +0000)]
Big progress

16 years agosnapshot
Enrico Tassi [Thu, 22 Nov 2007 13:29:20 +0000 (13:29 +0000)]
snapshot

16 years agoVery incomplete example of simple calculus exercises in Matita.
Claudio Sacerdoti Coen [Wed, 21 Nov 2007 16:16:58 +0000 (16:16 +0000)]
Very incomplete example of simple calculus exercises in Matita.

16 years ago...
Enrico Tassi [Tue, 20 Nov 2007 12:59:08 +0000 (12:59 +0000)]
...

16 years agoopps, a changelog was already there
Enrico Tassi [Tue, 20 Nov 2007 12:52:28 +0000 (12:52 +0000)]
opps, a changelog was already there

16 years agoBug fixed: local type declarations are not allowed in ocaml.
Claudio Sacerdoti Coen [Mon, 19 Nov 2007 18:16:25 +0000 (18:16 +0000)]
Bug fixed: local type declarations are not allowed in ocaml.

16 years ago...
Enrico Tassi [Mon, 19 Nov 2007 14:02:27 +0000 (14:02 +0000)]
...

16 years agoTowards chebyshev.
Andrea Asperti [Mon, 19 Nov 2007 11:55:54 +0000 (11:55 +0000)]
Towards chebyshev.

16 years agoThe axiom can be proved. Just follow the hint.
Claudio Sacerdoti Coen [Sun, 18 Nov 2007 18:18:02 +0000 (18:18 +0000)]
The axiom can be proved. Just follow the hint.

16 years agofixed bugs found by csc
Enrico Tassi [Sat, 17 Nov 2007 18:27:15 +0000 (18:27 +0000)]
fixed bugs found by csc

16 years agomoved to pkg-ocaml-maint
Enrico Tassi [Sat, 17 Nov 2007 17:33:43 +0000 (17:33 +0000)]
moved to pkg-ocaml-maint

16 years agoSome notes for Enrico.
Claudio Sacerdoti Coen [Fri, 16 Nov 2007 20:49:49 +0000 (20:49 +0000)]
Some notes for Enrico.

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 19:39:34 +0000 (19:39 +0000)]
...

16 years agohidded publish-devel button, too dangerous for the casual user
Enrico Tassi [Fri, 16 Nov 2007 19:34:32 +0000 (19:34 +0000)]
hidded publish-devel button, too dangerous for the casual user

16 years agohidded all hbugs related stuff
Enrico Tassi [Fri, 16 Nov 2007 19:32:12 +0000 (19:32 +0000)]
hidded all hbugs related stuff

16 years agofrom the tarball removed all contribs, they used to weight more than 1MB
Enrico Tassi [Fri, 16 Nov 2007 18:47:49 +0000 (18:47 +0000)]
from the tarball removed all contribs, they used to weight more than 1MB
and were not compiled nor installed

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 18:36:44 +0000 (18:36 +0000)]
...

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 14:34:33 +0000 (14:34 +0000)]
...

16 years agonocomposites
Enrico Tassi [Fri, 16 Nov 2007 14:24:38 +0000 (14:24 +0000)]
nocomposites

16 years agocompose tactic restore and added nocomposites keyword
Enrico Tassi [Fri, 16 Nov 2007 14:24:24 +0000 (14:24 +0000)]
compose tactic restore and added nocomposites keyword

16 years agomore cleanup
Enrico Tassi [Fri, 16 Nov 2007 14:12:48 +0000 (14:12 +0000)]
more cleanup