]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 11:15:04 +0000 (11:15 +0000)]
...

16 years agoadded recommends graphvi
Enrico Tassi [Fri, 16 Nov 2007 10:21:11 +0000 (10:21 +0000)]
added recommends graphvi

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 10:10:11 +0000 (10:10 +0000)]
...

16 years agoxxx
Enrico Tassi [Fri, 16 Nov 2007 10:08:08 +0000 (10:08 +0000)]
xxx

16 years agoadded homepage field in control
Enrico Tassi [Fri, 16 Nov 2007 10:02:48 +0000 (10:02 +0000)]
added homepage field in control

16 years agofix
Enrico Tassi [Fri, 16 Nov 2007 09:56:38 +0000 (09:56 +0000)]
fix

16 years agofix -noinnertypes set to true!
Enrico Tassi [Fri, 16 Nov 2007 09:33:37 +0000 (09:33 +0000)]
fix -noinnertypes set to true!

16 years agoremoved dummy MATITA_CFLAGS assignement
Enrico Tassi [Fri, 16 Nov 2007 09:11:50 +0000 (09:11 +0000)]
removed dummy MATITA_CFLAGS assignement

16 years agoadded default for matita.noiinertypes
Enrico Tassi [Fri, 16 Nov 2007 09:04:05 +0000 (09:04 +0000)]
added default for matita.noiinertypes

16 years agomenu fised
Enrico Tassi [Fri, 16 Nov 2007 08:56:55 +0000 (08:56 +0000)]
menu fised

16 years agopropagation of noinnertypes to matitac
Enrico Tassi [Fri, 16 Nov 2007 08:51:34 +0000 (08:51 +0000)]
propagation of noinnertypes to matitac

16 years agoadded -noinnertypes
Enrico Tassi [Fri, 16 Nov 2007 08:49:23 +0000 (08:49 +0000)]
added -noinnertypes

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 08:06:40 +0000 (08:06 +0000)]
...

16 years agocleanup
Enrico Tassi [Thu, 15 Nov 2007 17:15:05 +0000 (17:15 +0000)]
cleanup

16 years agocleanup
Enrico Tassi [Thu, 15 Nov 2007 17:14:37 +0000 (17:14 +0000)]
cleanup

16 years agodeclared eq_sym as a coercion and added 2 lemmas for rewriting #
Enrico Tassi [Thu, 15 Nov 2007 17:13:51 +0000 (17:13 +0000)]
declared eq_sym as a coercion and added 2 lemmas for rewriting #

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 16:35:08 +0000 (16:35 +0000)]
...

16 years agoautobatch => [auto]
Enrico Tassi [Thu, 15 Nov 2007 15:35:16 +0000 (15:35 +0000)]
autobatch => [auto]

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 15:27:54 +0000 (15:27 +0000)]
...

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 15:22:23 +0000 (15:22 +0000)]
...

16 years agoremoved prerr_endline
Enrico Tassi [Thu, 15 Nov 2007 13:44:43 +0000 (13:44 +0000)]
removed prerr_endline

16 years agoremoved ugly prerr_endline
Enrico Tassi [Thu, 15 Nov 2007 13:33:53 +0000 (13:33 +0000)]
removed ugly prerr_endline

16 years agoadded --version to allow help2man
Enrico Tassi [Thu, 15 Nov 2007 13:22:41 +0000 (13:22 +0000)]
added --version to allow help2man

16 years agoadded manpages
Enrico Tassi [Thu, 15 Nov 2007 13:22:13 +0000 (13:22 +0000)]
added manpages

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 11:07:14 +0000 (11:07 +0000)]
...