]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agoBug fixed: parsing errors were ignored by matitac since the EOI was not
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 15:41:51 +0000 (15:41 +0000)]
Bug fixed: parsing errors were ignored by matitac since the EOI was not
required to terminate the list of commands!

19 years agoBug fixed (that used to throw away a metasenv :-(
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 14:41:07 +0000 (14:41 +0000)]
Bug fixed (that used to throw away a metasenv :-(

19 years agofix
Enrico Tassi [Wed, 15 Jun 2005 14:07:33 +0000 (14:07 +0000)]
fix

19 years agorenamed clientHTTP to http_getter_wget
Stefano Zacchiroli [Wed, 15 Jun 2005 13:35:49 +0000 (13:35 +0000)]
renamed clientHTTP to http_getter_wget

19 years agowe no longer use pxp
Stefano Zacchiroli [Wed, 15 Jun 2005 12:56:49 +0000 (12:56 +0000)]
we no longer use pxp

19 years agosupport for the new tactics lapply and fwd
Ferruccio Guidi [Wed, 15 Jun 2005 12:42:21 +0000 (12:42 +0000)]
support for the new tactics lapply and fwd
used in forward reasoning

19 years agoenable static linking of C stub code
Stefano Zacchiroli [Wed, 15 Jun 2005 12:39:52 +0000 (12:39 +0000)]
enable static linking of C stub code

19 years agoversion 0.7.1-1
Stefano Zacchiroli [Wed, 15 Jun 2005 12:39:33 +0000 (12:39 +0000)]
version 0.7.1-1

19 years ago- better printing of modifiers
Stefano Zacchiroli [Wed, 15 Jun 2005 12:39:04 +0000 (12:39 +0000)]
- better printing of modifiers
- quit on window destroy

19 years agobeginning of the tactics lapply and fwd
Ferruccio Guidi [Wed, 15 Jun 2005 12:38:41 +0000 (12:38 +0000)]
beginning of the tactics lapply and fwd
used to support forward reasoning

19 years agosync with new typecheck prototype (no more univ graph)
Enrico Tassi [Wed, 15 Jun 2005 12:24:06 +0000 (12:24 +0000)]
sync with new typecheck prototype (no more univ graph)

19 years ago...
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 12:15:26 +0000 (12:15 +0000)]
...

19 years agoapply_tac used to calculate the type of the term before generalizing on explicit...
Enrico Tassi [Wed, 15 Jun 2005 11:39:45 +0000 (11:39 +0000)]
apply_tac used to calculate the type of the term before generalizing on explicit name subts

19 years agoare_convertible on MutCase was no longer checking the match arguments
Enrico Tassi [Wed, 15 Jun 2005 11:38:55 +0000 (11:38 +0000)]
are_convertible on MutCase was no longer checking the match arguments
convertibility.

19 years agoported to latest registry interface
Stefano Zacchiroli [Wed, 15 Jun 2005 11:32:23 +0000 (11:32 +0000)]
ported to latest registry interface

19 years ago- support for multiple bindings of the same key, accessible via get_list
Stefano Zacchiroli [Wed, 15 Jun 2005 11:31:15 +0000 (11:31 +0000)]
- support for multiple bindings of the same key, accessible via get_list
- changed get_opt interface so that marshallers/unmarshallers are needed
  instead of getters/setters

19 years agoRefinement of CurrentProof did not check whether the type is a type.
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 11:22:55 +0000 (11:22 +0000)]
Refinement of CurrentProof did not check whether the type is a type.
As a consequence it was possible to do "theorem t: 0" :-)

19 years agoBig commit and major code clean-up:
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 10:55:08 +0000 (10:55 +0000)]
Big commit and major code clean-up:
1. added a refine function for objects
2. added a disambiguation function for objects
3. MatitaEngine now uses the disambiguation function for objects
4. added CicTypeChecker.typecheck_obj to typecheck an object and add it
   to the environment

19 years agocomments syntax changed
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 10:54:43 +0000 (10:54 +0000)]
comments syntax changed

19 years agoincomplete proof completed.
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 10:54:22 +0000 (10:54 +0000)]
incomplete proof completed.

19 years agouse META helm-registry package, load sample.xml and open Helm_registry
Stefano Zacchiroli [Wed, 15 Jun 2005 09:06:29 +0000 (09:06 +0000)]
use META helm-registry package, load sample.xml and open Helm_registry

19 years agonow something works...
Alberto Griggio [Wed, 15 Jun 2005 08:34:46 +0000 (08:34 +0000)]
now something works...

19 years ago* no more %% comments
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 16:19:09 +0000 (16:19 +0000)]
* no more %% comments
* parsed comments must start with "(**b" where b is any blank
  and must be termianted by "*)"

19 years agoNo more %% comments.
Claudio Sacerdoti Coen [Tue, 14 Jun 2005 16:18:39 +0000 (16:18 +0000)]
No more %% comments.

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.