]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agoconcrete syntax for goal patterns
Enrico Tassi [Fri, 17 Jun 2005 14:58:02 +0000 (14:58 +0000)]
concrete syntax for goal patterns

19 years agoadded support for patterns current goal
Enrico Tassi [Fri, 17 Jun 2005 14:57:43 +0000 (14:57 +0000)]
added support for patterns current goal

19 years agochanged select so that it returns a list of pairs <number of binders crossed, term>
Enrico Tassi [Fri, 17 Jun 2005 14:56:24 +0000 (14:56 +0000)]
changed select so that it returns a list of pairs <number of binders crossed, term>

19 years agoprofiling experiments...
Alberto Griggio [Fri, 17 Jun 2005 13:28:27 +0000 (13:28 +0000)]
profiling experiments...

19 years agomore strings to UriManager.uri
Claudio Sacerdoti Coen [Fri, 17 Jun 2005 13:28:22 +0000 (13:28 +0000)]
more strings to UriManager.uri

19 years agomany strings that are supposed to be URIs are now UriManager.uri
Claudio Sacerdoti Coen [Fri, 17 Jun 2005 13:05:08 +0000 (13:05 +0000)]
many strings that are supposed to be URIs are now UriManager.uri

19 years agoremoved spurious entry gtkrc
Stefano Zacchiroli [Fri, 17 Jun 2005 07:49:25 +0000 (07:49 +0000)]
removed spurious entry gtkrc

19 years agoLocally implemented print_context replaced by CicPp.ppcontext.
Claudio Sacerdoti Coen [Thu, 16 Jun 2005 16:40:55 +0000 (16:40 +0000)]
Locally implemented print_context replaced by CicPp.ppcontext.

19 years agoA cleaned version of auto_tac_new.
Andrea Asperti [Thu, 16 Jun 2005 16:34:24 +0000 (16:34 +0000)]
A cleaned version of auto_tac_new.

19 years agoadded depth and width (optional) parameters to auto_tac_new
Stefano Zacchiroli [Thu, 16 Jun 2005 15:11:56 +0000 (15:11 +0000)]
added depth and width (optional) parameters to auto_tac_new

19 years agouses auto_tac_new instead of auto_tac
Stefano Zacchiroli [Thu, 16 Jun 2005 15:11:32 +0000 (15:11 +0000)]
uses auto_tac_new instead of auto_tac

19 years agoDead code clean-up.
Claudio Sacerdoti Coen [Thu, 16 Jun 2005 14:16:21 +0000 (14:16 +0000)]
Dead code clean-up.

19 years agoDead code for packing/unpacking (usually just a big hack) commented out
Claudio Sacerdoti Coen [Thu, 16 Jun 2005 14:14:41 +0000 (14:14 +0000)]
Dead code for packing/unpacking (usually just a big hack) commented out
(hopefully forever).

19 years agoDead code clean-up.
Claudio Sacerdoti Coen [Thu, 16 Jun 2005 14:07:33 +0000 (14:07 +0000)]
Dead code clean-up.

19 years agoadded decrease and increase font size fantafeature
Enrico Tassi [Thu, 16 Jun 2005 11:55:21 +0000 (11:55 +0000)]
added decrease and increase font size fantafeature

19 years agoadded utility to dump some tables of the db on mowgli
Enrico Tassi [Thu, 16 Jun 2005 09:25:50 +0000 (09:25 +0000)]
added utility to dump some tables of the db on mowgli
(useful to export metadata to laptops)

19 years agomatita.conf.xml added
Claudio Sacerdoti Coen [Thu, 16 Jun 2005 08:06:35 +0000 (08:06 +0000)]
matita.conf.xml added

19 years agoremoved again (I added it by error :-(
Claudio Sacerdoti Coen [Thu, 16 Jun 2005 08:06:00 +0000 (08:06 +0000)]
removed again (I added it by error :-(

19 years ago* parsing errors in tests were not detected and the rest of the file was
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 17:05:53 +0000 (17:05 +0000)]
* parsing errors in tests were not detected and the rest of the file was
  ignored!!!! Tests fixed
* a few interactive tests moved to tests/interactive to avoid regression
  testing over them (for now...)

19 years agoDTD for attributes revised.
Stefano Zacchiroli [Wed, 15 Jun 2005 16:54:46 +0000 (16:54 +0000)]
DTD for attributes revised.
New syntax:
 <attributes>
  <class type="..">
   ...
  </class>
  <generated />
 </attributes>
where the ... are the arguments of the class and the class and generated
elements are optional. For the "elim" class the only argument is the SORT.
For the "record" class the arguments are a list of <field name=".."/>

19 years agoSyntax of <attributes>...</attributes> improved to allow arguments for
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 16:49:53 +0000 (16:49 +0000)]
Syntax of <attributes>...</attributes> improved to allow arguments for
classes.

19 years agoDTD for attributes revised.
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 16:37:16 +0000 (16:37 +0000)]
DTD for attributes revised.
New syntax:
 <attributes>
  <class type="..">
   ...
  </class>
  <generated />
 </attributes>
where the ... are the arguments of the class and the class and generated
elements are optional. For the "elim" class the only argument is the SORT.
For the "record" class the arguments are a list of <field name=".."/>

19 years agoThe `Record class now records also the name of the fields
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 16:18:12 +0000 (16:18 +0000)]
The `Record class now records also the name of the fields
(used to generate the projections)

19 years agoa parser error is now logged as an error!
Claudio Sacerdoti Coen [Wed, 15 Jun 2005 15:43:06 +0000 (15:43 +0000)]
a parser error is now logged as an error!

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.