]>
matita.cs.unibo.it Git - helm.git/log
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 08:13:59 +0000 (08:13 +0000)]
incomplete proof terminated
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 08:12:04 +0000 (08:12 +0000)]
qed missing
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 08:11:12 +0000 (08:11 +0000)]
Bug fixed: when the final proof_status is not No_proof matitac returns -1.
Enrico Tassi [Tue, 14 Jun 2005 07:57:51 +0000 (07:57 +0000)]
added fullscreen menu item
Stefano Zacchiroli [Mon, 13 Jun 2005 15:25:49 +0000 (15:25 +0000)]
integrated lablgtksourceview
Enrico Tassi [Mon, 13 Jun 2005 15:22:36 +0000 (15:22 +0000)]
cosmetic fix
Stefano Zacchiroli [Mon, 13 Jun 2005 14:56:48 +0000 (14:56 +0000)]
- no longer build mathql per default
- moved cic_notation after cic_transformation
Enrico Tassi [Mon, 13 Jun 2005 14:54:18 +0000 (14:54 +0000)]
renamed
Enrico Tassi [Mon, 13 Jun 2005 14:48:34 +0000 (14:48 +0000)]
fix
Enrico Tassi [Mon, 13 Jun 2005 14:45:57 +0000 (14:45 +0000)]
F2 hides the tactics buttons bar
Stefano Zacchiroli [Mon, 13 Jun 2005 14:20:04 +0000 (14:20 +0000)]
- new minor version
- rebuilt against today lablgtk2 CVS snapshot
Stefano Zacchiroli [Mon, 13 Jun 2005 14:19:50 +0000 (14:19 +0000)]
ported to official (guessed) version of lablgtk2
Stefano Zacchiroli [Mon, 13 Jun 2005 14:19:27 +0000 (14:19 +0000)]
better clean up on dist
Stefano Zacchiroli [Mon, 13 Jun 2005 14:19:24 +0000 (14:19 +0000)]
moved the annoying debugging print to test
Stefano Zacchiroli [Mon, 13 Jun 2005 13:40:34 +0000 (13:40 +0000)]
ported to lablgtk2 2.4.0+2005.06.13-1
Stefano Zacchiroli [Mon, 13 Jun 2005 13:23:29 +0000 (13:23 +0000)]
ported to latest lablgtk2 snapshot (13/06/2005) in which Garrigue
applied my patch about *_skel
Enrico Tassi [Mon, 13 Jun 2005 12:38:52 +0000 (12:38 +0000)]
fix
Enrico Tassi [Mon, 13 Jun 2005 12:30:08 +0000 (12:30 +0000)]
added syntax hilight for temperino
Enrico Tassi [Mon, 13 Jun 2005 12:29:37 +0000 (12:29 +0000)]
removed prerr_endline
Enrico Tassi [Mon, 13 Jun 2005 12:20:24 +0000 (12:20 +0000)]
fix
Enrico Tassi [Mon, 13 Jun 2005 12:20:06 +0000 (12:20 +0000)]
error
Enrico Tassi [Mon, 13 Jun 2005 09:56:21 +0000 (09:56 +0000)]
moved to xmlPushParser
Enrico Tassi [Mon, 13 Jun 2005 09:27:36 +0000 (09:27 +0000)]
fixed error in comment
Stefano Zacchiroli [Sat, 11 Jun 2005 19:25:43 +0000 (19:25 +0000)]
rewritten makefile and debian packaging: .deb ready!
Stefano Zacchiroli [Sat, 11 Jun 2005 12:18:59 +0000 (12:18 +0000)]
added an 'a parameter to mpresentation type so that it and boxes could
be used in a mutual recursive fashoin (boxes inside mpresentation inside
boxes ...) needed by cic_notation
Stefano Zacchiroli [Sat, 11 Jun 2005 10:36:47 +0000 (10:36 +0000)]
ocaml 3.08.3 commit
Stefano Zacchiroli [Sat, 11 Jun 2005 10:23:27 +0000 (10:23 +0000)]
fixed segfault issue with matching bracket search
Stefano Zacchiroli [Sat, 11 Jun 2005 10:22:54 +0000 (10:22 +0000)]
first checkin of debian stuff, something done, but still almost copy and
paste from lablgtkmathview
Stefano Zacchiroli [Fri, 10 Jun 2005 17:57:50 +0000 (17:57 +0000)]
snapshort
- bound (hidden) function for creation of language from file
- bound find_matching_bracket
- changed license to LGPL
Enrico Tassi [Fri, 10 Jun 2005 16:57:50 +0000 (16:57 +0000)]
added_test
Enrico Tassi [Fri, 10 Jun 2005 16:57:33 +0000 (16:57 +0000)]
added records
Enrico Tassi [Fri, 10 Jun 2005 16:53:21 +0000 (16:53 +0000)]
added mk_rel
Enrico Tassi [Fri, 10 Jun 2005 16:52:07 +0000 (16:52 +0000)]
added records pp, ast and fixed a bug in match with only one branch
Enrico Tassi [Fri, 10 Jun 2005 16:48:33 +0000 (16:48 +0000)]
added record generation modules
Enrico Tassi [Fri, 10 Jun 2005 16:48:11 +0000 (16:48 +0000)]
added record generation module
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 16:02:39 +0000 (16:02 +0000)]
The type of the left parameters of an inductive type can now be omitted.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 15:47:37 +0000 (15:47 +0000)]
Got rid of a few bugs.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 15:45:35 +0000 (15:45 +0000)]
Got rid of a few warnings.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 15:39:29 +0000 (15:39 +0000)]
Got rid of a few warnings.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 14:51:04 +0000 (14:51 +0000)]
an assert failure changed to an exception and a bit of code cleanupt
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 14:31:43 +0000 (14:31 +0000)]
The user is no longer obliged to give the types for definitions.
Alberto Griggio [Fri, 10 Jun 2005 14:16:29 +0000 (14:16 +0000)]
integrated indexing.ml, breaks everything :-P (previous working version tagged PRE_INDEXING_1)
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 14:11:59 +0000 (14:11 +0000)]
debugging to false
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 14:03:41 +0000 (14:03 +0000)]
* (Head) beta reduction functions factorized
* the type inferred for a match both in the kernel and in the refiner
are now beta reduced
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 13:42:47 +0000 (13:42 +0000)]
More debugging infos.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 13:00:51 +0000 (13:00 +0000)]
...
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 12:55:23 +0000 (12:55 +0000)]
unshare.ml*
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 12:54:44 +0000 (12:54 +0000)]
Complete unsharing of terms.
Stefano Zacchiroli [Fri, 10 Jun 2005 12:35:49 +0000 (12:35 +0000)]
- bound GtkSourceLanguagesManager (only get_lang..from_mime_type)
Stefano Zacchiroli [Fri, 10 Jun 2005 11:38:53 +0000 (11:38 +0000)]
snaphot
- better creation of GtkSourceView (using C constructor)
- bound GtkSourceLanguage
- preliminary binding of GtkSourceLanguagesManager
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 11:06:24 +0000 (11:06 +0000)]
head_beta_reduce used to create applications of applications. Fixed.
head_beta_reduce renamed to beta_reduce (since it performs full beta reduction).
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 09:26:29 +0000 (09:26 +0000)]
...
Stefano Zacchiroli [Thu, 9 Jun 2005 21:12:20 +0000 (21:12 +0000)]
added source_view ?text constructor parameter
Stefano Zacchiroli [Thu, 9 Jun 2005 21:12:04 +0000 (21:12 +0000)]
test file
Stefano Zacchiroli [Thu, 9 Jun 2005 21:11:52 +0000 (21:11 +0000)]
load "test.txt" and show it in a scrolled win
Stefano Zacchiroli [Thu, 9 Jun 2005 20:48:04 +0000 (20:48 +0000)]
snapshot
- implemented many methods of GtkSourceBuffer
- fixed creation of GtkSourceView (no longer assert failure on undo)
Alberto Griggio [Thu, 9 Jun 2005 17:19:17 +0000 (17:19 +0000)]
prima implementazione di demodulate, superposition_left e superposition_right
con gli "indici"...
Alberto Griggio [Thu, 9 Jun 2005 17:17:30 +0000 (17:17 +0000)]
cambiato il tipo equality, aggiunto l'ordinamento tra left e right
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:28:34 +0000 (16:28 +0000)]
...
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:24:24 +0000 (16:24 +0000)]
test_instance.ma moved to interactive/ (whose tests are not executed for
regression testing)
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:23:05 +0000 (16:23 +0000)]
intro ==> intros
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:22:51 +0000 (16:22 +0000)]
Error message improved.
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:09:55 +0000 (16:09 +0000)]
Now CicMetaSubst.delift_rels restricts the Metas when a failure is faced.
This closes yet another bug in the inference of the outtype for matches.
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:08:57 +0000 (16:08 +0000)]
No more explicit types for the branches of the matches: all the bugs
preventing automatic type inference have been fixed.
Stefano Zacchiroli [Thu, 9 Jun 2005 15:34:11 +0000 (15:34 +0000)]
snapshot
- almost fully bound SourceView
- started binding of SourceBuffer
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 15:04:49 +0000 (15:04 +0000)]
CicSubstitution.delift ==> CicMetaSubst.delift_rels
(since it will need to restrict metavariables in case of Rel capture)
Stefano Zacchiroli [Thu, 9 Jun 2005 14:11:13 +0000 (14:11 +0000)]
lablgtksourceview: first checkin, almost nothing bound ...
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 13:41:22 +0000 (13:41 +0000)]
Exception raised by delift changed:
Failure ==> DeliftingWouldCaptureAFreeVariable
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 13:03:49 +0000 (13:03 +0000)]
Debugging code removed.
Enrico Tassi [Thu, 9 Jun 2005 11:46:58 +0000 (11:46 +0000)]
added debug item for coercion
Enrico Tassi [Thu, 9 Jun 2005 11:46:28 +0000 (11:46 +0000)]
added \n to "file saved" message
Enrico Tassi [Thu, 9 Jun 2005 11:45:45 +0000 (11:45 +0000)]
added whd before uri_of_term
Enrico Tassi [Thu, 9 Jun 2005 11:44:27 +0000 (11:44 +0000)]
removed debug prints
Enrico Tassi [Thu, 9 Jun 2005 11:43:40 +0000 (11:43 +0000)]
fixed remove_coercion
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 10:43:44 +0000 (10:43 +0000)]
andrea.ma removed (superseded by match.ma)
Andrea Asperti [Thu, 9 Jun 2005 10:33:47 +0000 (10:33 +0000)]
Updated to the new syntax for match.
Stefano Zacchiroli [Thu, 9 Jun 2005 07:35:30 +0000 (07:35 +0000)]
simplified cicBrowser: whelp bar is now always visible
Stefano Zacchiroli [Wed, 8 Jun 2005 20:17:03 +0000 (20:17 +0000)]
- handles about:* uris in cicBrowser
- added comboboxentry in cicBrowser (still ugly ...)
Stefano Zacchiroli [Wed, 8 Jun 2005 19:21:33 +0000 (19:21 +0000)]
fixed history handling: now both "home" and link reached via href are
correctly stored and remembered in history
Stefano Zacchiroli [Wed, 8 Jun 2005 16:53:28 +0000 (16:53 +0000)]
rewritten cicBrowser handling of uri text entry, still some issued with browser
history
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:50:36 +0000 (16:50 +0000)]
The type of a top-level "let rec" can be optional.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:49:40 +0000 (16:49 +0000)]
Let's try to make the "let rec" construct infer its arguments.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:36:55 +0000 (16:36 +0000)]
Syntax for top-level "let rec" fixed.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:32:50 +0000 (16:32 +0000)]
Using the lighter syntax for "let recs".
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:31:02 +0000 (16:31 +0000)]
Using the top-level syntax for let-rec definitions.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:30:04 +0000 (16:30 +0000)]
The file is now well formed.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:19:14 +0000 (16:19 +0000)]
New syntax (again) for let rec binders:
let rec f x y (z,w:T) h (c:T) = ...
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:11:00 +0000 (16:11 +0000)]
New lighter syntax for "let rec".
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:09:08 +0000 (16:09 +0000)]
Bug fixed: a symbol must be formed of just one (unicode) character.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:06:47 +0000 (16:06 +0000)]
Query results were erroneously tagged as directories.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 15:24:24 +0000 (15:24 +0000)]
1. syntax of match changed
2. syntax of the bindings of "let rec" made lighter
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 15:17:15 +0000 (15:17 +0000)]
Yet another bug fixed in the inference of the outtype for match: convertibility
was used in place of unification, making type inference much less powerful
in several useful cases.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 14:11:02 +0000 (14:11 +0000)]
The getter maps are now dumped also if matitac exits abruptly.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 14:00:35 +0000 (14:00 +0000)]
Added new target "make tests" for regression testing.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 13:47:53 +0000 (13:47 +0000)]
Fixed a few bugs in the inference of the outtype for a match.
In particular the instances of the left parameter that occur in the
outtype were not lifted properly because of the abstractions that correspond
to the right parameters.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 10:52:20 +0000 (10:52 +0000)]
Fixed inference of outtype for match when the inductive type has left and/or
right parameters.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 10:50:31 +0000 (10:50 +0000)]
Harder test (with empty inductive types and left and right arguments to
inductive types). It does not compile yet.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 10:49:49 +0000 (10:49 +0000)]
More informative error message.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 09:45:59 +0000 (09:45 +0000)]
clean now also performs clean_metas (since make also creates the metas)
Stefano Zacchiroli [Wed, 8 Jun 2005 09:10:17 +0000 (09:10 +0000)]
added icons to entries shown in cicbrowser so that directories are
distinguishable from objects