]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agoparentheses allowed inside comments
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 16:01:05 +0000 (16:01 +0000)]
parentheses allowed inside comments

19 years agotest_lexer and test_parser compiled by default
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 15:54:43 +0000 (15:54 +0000)]
test_lexer and test_parser compiled by default

19 years agouses XmlPushParser instead of PXP
Stefano Zacchiroli [Tue, 14 Jun 2005 13:47:23 +0000 (13:47 +0000)]
uses XmlPushParser instead of PXP

19 years agofinally we understood how to properly link ocaml bindings ....
Stefano Zacchiroli [Tue, 14 Jun 2005 13:29:06 +0000 (13:29 +0000)]
finally we understood how to properly link ocaml bindings ....

19 years agofix
Enrico Tassi [Tue, 14 Jun 2005 11:54:31 +0000 (11:54 +0000)]
fix

19 years agoremoved ocaml-pxp
Enrico Tassi [Tue, 14 Jun 2005 11:46:43 +0000 (11:46 +0000)]
removed ocaml-pxp

19 years agohack to compile on gazelle
Enrico Tassi [Tue, 14 Jun 2005 11:44:58 +0000 (11:44 +0000)]
hack to compile on gazelle

19 years agodone two items
Stefano Zacchiroli [Tue, 14 Jun 2005 11:19:23 +0000 (11:19 +0000)]
done two items

19 years agodon't build pxp (no longer needed), cic_annotations (triassic dinosaur),
Stefano Zacchiroli [Tue, 14 Jun 2005 11:16:36 +0000 (11:16 +0000)]
don't build pxp (no longer needed), cic_annotations (triassic dinosaur),
hbugs (coming soon ...)

19 years agoremoved dependencies on Pxp
Stefano Zacchiroli [Tue, 14 Jun 2005 11:15:38 +0000 (11:15 +0000)]
removed dependencies on Pxp

19 years agoremoved dependency on cicPxpParser
Stefano Zacchiroli [Tue, 14 Jun 2005 11:15:26 +0000 (11:15 +0000)]
removed dependency on cicPxpParser

19 years agouses XmlPushParser instead of Pxp for parsing getter resolve answer
Stefano Zacchiroli [Tue, 14 Jun 2005 11:15:07 +0000 (11:15 +0000)]
uses XmlPushParser instead of Pxp for parsing getter resolve answer

19 years agoincomplete proof completed
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 08:20:37 +0000 (08:20 +0000)]
incomplete proof completed

19 years agotypo fixed: simmetry ==> symmetry
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 08:18:18 +0000 (08:18 +0000)]
typo fixed: simmetry ==> symmetry

19 years agoincomplete proof terminated
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 08:13:59 +0000 (08:13 +0000)]
incomplete proof terminated

19 years agoqed missing
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 08:12:04 +0000 (08:12 +0000)]
qed missing

19 years agoBug fixed: when the final proof_status is not No_proof matitac returns -1.
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.

19 years agoadded fullscreen menu item
Enrico Tassi [Tue, 14 Jun 2005 07:57:51 +0000 (07:57 +0000)]
added fullscreen menu item

19 years agointegrated lablgtksourceview
Stefano Zacchiroli [Mon, 13 Jun 2005 15:25:49 +0000 (15:25 +0000)]
integrated lablgtksourceview

19 years agocosmetic fix
Enrico Tassi [Mon, 13 Jun 2005 15:22:36 +0000 (15:22 +0000)]
cosmetic fix

19 years ago- no longer build mathql per default
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

19 years agorenamed
Enrico Tassi [Mon, 13 Jun 2005 14:54:18 +0000 (14:54 +0000)]
renamed

19 years agofix
Enrico Tassi [Mon, 13 Jun 2005 14:48:34 +0000 (14:48 +0000)]
fix

19 years agoF2 hides the tactics buttons bar
Enrico Tassi [Mon, 13 Jun 2005 14:45:57 +0000 (14:45 +0000)]
F2 hides the tactics buttons bar

19 years ago- new minor version
Stefano Zacchiroli [Mon, 13 Jun 2005 14:20:04 +0000 (14:20 +0000)]
- new minor version
- rebuilt against today lablgtk2 CVS snapshot

19 years agoported to official (guessed) version of lablgtk2
Stefano Zacchiroli [Mon, 13 Jun 2005 14:19:50 +0000 (14:19 +0000)]
ported to official (guessed) version of lablgtk2

19 years agobetter clean up on dist
Stefano Zacchiroli [Mon, 13 Jun 2005 14:19:27 +0000 (14:19 +0000)]
better clean up on dist

19 years agomoved the annoying debugging print to test
Stefano Zacchiroli [Mon, 13 Jun 2005 14:19:24 +0000 (14:19 +0000)]
moved the annoying debugging print to test

19 years agoported to lablgtk2 2.4.0+2005.06.13-1
Stefano Zacchiroli [Mon, 13 Jun 2005 13:40:34 +0000 (13:40 +0000)]
ported to lablgtk2 2.4.0+2005.06.13-1

19 years agoported to latest lablgtk2 snapshot (13/06/2005) in which Garrigue
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

19 years agofix
Enrico Tassi [Mon, 13 Jun 2005 12:38:52 +0000 (12:38 +0000)]
fix

19 years agoadded syntax hilight for temperino
Enrico Tassi [Mon, 13 Jun 2005 12:30:08 +0000 (12:30 +0000)]
added syntax hilight for temperino

19 years agoremoved prerr_endline
Enrico Tassi [Mon, 13 Jun 2005 12:29:37 +0000 (12:29 +0000)]
removed prerr_endline

19 years agofix
Enrico Tassi [Mon, 13 Jun 2005 12:20:24 +0000 (12:20 +0000)]
fix

19 years agoerror
Enrico Tassi [Mon, 13 Jun 2005 12:20:06 +0000 (12:20 +0000)]
error

19 years agomoved to xmlPushParser
Enrico Tassi [Mon, 13 Jun 2005 09:56:21 +0000 (09:56 +0000)]
moved to xmlPushParser

19 years agofixed error in comment
Enrico Tassi [Mon, 13 Jun 2005 09:27:36 +0000 (09:27 +0000)]
fixed error in comment

19 years agorewritten makefile and debian packaging: .deb ready!
Stefano Zacchiroli [Sat, 11 Jun 2005 19:25:43 +0000 (19:25 +0000)]
rewritten makefile and debian packaging: .deb ready!

19 years agoadded an 'a parameter to mpresentation type so that it and boxes could
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

19 years agoocaml 3.08.3 commit
Stefano Zacchiroli [Sat, 11 Jun 2005 10:36:47 +0000 (10:36 +0000)]
ocaml 3.08.3 commit

19 years agofixed segfault issue with matching bracket search
Stefano Zacchiroli [Sat, 11 Jun 2005 10:23:27 +0000 (10:23 +0000)]
fixed segfault issue with matching bracket search

19 years agofirst checkin of debian stuff, something done, but still almost copy and
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

19 years agosnapshort
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

19 years agoadded_test
Enrico Tassi [Fri, 10 Jun 2005 16:57:50 +0000 (16:57 +0000)]
added_test

19 years agoadded records
Enrico Tassi [Fri, 10 Jun 2005 16:57:33 +0000 (16:57 +0000)]
added records

19 years agoadded mk_rel
Enrico Tassi [Fri, 10 Jun 2005 16:53:21 +0000 (16:53 +0000)]
added mk_rel

19 years agoadded records pp, ast and fixed a bug in match with only one branch
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

19 years agoadded record generation modules
Enrico Tassi [Fri, 10 Jun 2005 16:48:33 +0000 (16:48 +0000)]
added record generation modules

19 years agoadded record generation module
Enrico Tassi [Fri, 10 Jun 2005 16:48:11 +0000 (16:48 +0000)]
added record generation module

19 years agoThe type of the left parameters of an inductive type can now be omitted.
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.

19 years agoGot rid of a few bugs.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 15:47:37 +0000 (15:47 +0000)]
Got rid of a few bugs.

19 years agoGot rid of a few warnings.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 15:45:35 +0000 (15:45 +0000)]
Got rid of a few warnings.

19 years agoGot 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.

19 years agoan assert failure changed to an exception and a bit of code cleanupt
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

19 years agoThe user is no longer obliged to give the types for definitions.
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.

19 years agointegrated indexing.ml, breaks everything :-P (previous working version tagged PRE_IN...
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)

19 years agodebugging to false
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 14:11:59 +0000 (14:11 +0000)]
debugging to false

19 years ago* (Head) beta reduction functions factorized
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

19 years agoMore debugging infos.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 13:42:47 +0000 (13:42 +0000)]
More debugging infos.

19 years ago...
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 13:00:51 +0000 (13:00 +0000)]
...

19 years agounshare.ml*
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 12:55:23 +0000 (12:55 +0000)]
unshare.ml*

19 years agoComplete unsharing of terms.
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 12:54:44 +0000 (12:54 +0000)]
Complete unsharing of terms.

19 years ago- bound GtkSourceLanguagesManager (only get_lang..from_mime_type)
Stefano Zacchiroli [Fri, 10 Jun 2005 12:35:49 +0000 (12:35 +0000)]
- bound GtkSourceLanguagesManager (only get_lang..from_mime_type)

19 years agosnaphot
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

19 years agohead_beta_reduce used to create applications of applications. Fixed.
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).

19 years ago...
Claudio Sacerdoti Coen [Fri, 10 Jun 2005 09:26:29 +0000 (09:26 +0000)]
...

19 years agoadded source_view ?text constructor parameter
Stefano Zacchiroli [Thu, 9 Jun 2005 21:12:20 +0000 (21:12 +0000)]
added source_view ?text constructor parameter

19 years agotest file
Stefano Zacchiroli [Thu, 9 Jun 2005 21:12:04 +0000 (21:12 +0000)]
test file

19 years agoload "test.txt" and show it in a scrolled win
Stefano Zacchiroli [Thu, 9 Jun 2005 21:11:52 +0000 (21:11 +0000)]
load "test.txt" and show it in a scrolled win

19 years agosnapshot
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)

19 years agoprima implementazione di demodulate, superposition_left e superposition_right
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"...

19 years agocambiato il tipo equality, aggiunto l'ordinamento tra left e right
Alberto Griggio [Thu, 9 Jun 2005 17:17:30 +0000 (17:17 +0000)]
cambiato il tipo equality, aggiunto l'ordinamento tra left e right

19 years ago...
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:28:34 +0000 (16:28 +0000)]
...

19 years agotest_instance.ma moved to interactive/ (whose tests are not executed for
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)

19 years agointro ==> intros
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:23:05 +0000 (16:23 +0000)]
intro ==> intros

19 years agoError message improved.
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 16:22:51 +0000 (16:22 +0000)]
Error message improved.

19 years agoNow CicMetaSubst.delift_rels restricts the Metas when a failure is faced.
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.

19 years agoNo more explicit types for the branches of the matches: all the bugs
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.

19 years agosnapshot
Stefano Zacchiroli [Thu, 9 Jun 2005 15:34:11 +0000 (15:34 +0000)]
snapshot
- almost fully bound SourceView
- started binding of SourceBuffer

19 years agoCicSubstitution.delift ==> CicMetaSubst.delift_rels
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)

19 years agolablgtksourceview: first checkin, almost nothing bound ...
Stefano Zacchiroli [Thu, 9 Jun 2005 14:11:13 +0000 (14:11 +0000)]
lablgtksourceview: first checkin, almost nothing bound ...

19 years agoException raised by delift changed:
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 13:41:22 +0000 (13:41 +0000)]
Exception raised by delift changed:
Failure ==> DeliftingWouldCaptureAFreeVariable

19 years agoDebugging code removed.
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 13:03:49 +0000 (13:03 +0000)]
Debugging code removed.

19 years agoadded debug item for coercion
Enrico Tassi [Thu, 9 Jun 2005 11:46:58 +0000 (11:46 +0000)]
added debug item for coercion

19 years agoadded \n to "file saved" message
Enrico Tassi [Thu, 9 Jun 2005 11:46:28 +0000 (11:46 +0000)]
added \n to "file saved" message

19 years agoadded whd before uri_of_term
Enrico Tassi [Thu, 9 Jun 2005 11:45:45 +0000 (11:45 +0000)]
added whd before uri_of_term

19 years agoremoved debug prints
Enrico Tassi [Thu, 9 Jun 2005 11:44:27 +0000 (11:44 +0000)]
removed debug prints

19 years agofixed remove_coercion
Enrico Tassi [Thu, 9 Jun 2005 11:43:40 +0000 (11:43 +0000)]
fixed remove_coercion

19 years agoandrea.ma removed (superseded by match.ma)
Claudio Sacerdoti Coen [Thu, 9 Jun 2005 10:43:44 +0000 (10:43 +0000)]
andrea.ma removed (superseded by match.ma)

19 years agoUpdated to the new syntax for match.
Andrea Asperti [Thu, 9 Jun 2005 10:33:47 +0000 (10:33 +0000)]
Updated to the new syntax for match.

19 years agosimplified cicBrowser: whelp bar is now always visible
Stefano Zacchiroli [Thu, 9 Jun 2005 07:35:30 +0000 (07:35 +0000)]
simplified cicBrowser: whelp bar is now always visible

19 years ago- handles about:* uris in cicBrowser
Stefano Zacchiroli [Wed, 8 Jun 2005 20:17:03 +0000 (20:17 +0000)]
- handles about:* uris in cicBrowser
- added comboboxentry in cicBrowser (still ugly ...)

19 years agofixed history handling: now both "home" and link reached via href are
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

19 years agorewritten cicBrowser handling of uri text entry, still some issued with browser
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

19 years agoThe type of a top-level "let rec" can be optional.
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.

19 years agoLet's try to make the "let rec" construct infer its arguments.
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.

19 years agoSyntax for top-level "let rec" fixed.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:36:55 +0000 (16:36 +0000)]
Syntax for top-level "let rec" fixed.

19 years agoUsing the lighter syntax for "let recs".
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:32:50 +0000 (16:32 +0000)]
Using the lighter syntax for "let recs".

19 years agoUsing the top-level syntax for let-rec definitions.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:31:02 +0000 (16:31 +0000)]
Using the top-level syntax for let-rec definitions.

19 years agoThe file is now well formed.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:30:04 +0000 (16:30 +0000)]
The file is now well formed.