]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agoAdded a whd on ty in new_metasenv for apply, in order to be able
Andrea Asperti [Fri, 20 May 2005 15:24:18 +0000 (15:24 +0000)]
Added a whd on ty in new_metasenv for apply, in order to be able
to apply, e.g. H:(not A) to False.

19 years agoHint repaired (an erroneous commit by myself).
Andrea Asperti [Fri, 20 May 2005 09:13:34 +0000 (09:13 +0000)]
Hint repaired (an erroneous commit by myself).

19 years agofix
Enrico Tassi [Thu, 19 May 2005 13:19:27 +0000 (13:19 +0000)]
fix

19 years agoadded lpo term-ordering
Alberto Griggio [Thu, 19 May 2005 13:12:56 +0000 (13:12 +0000)]
added lpo term-ordering

19 years agovarious optimizations (to paramodulation and passive clause selection)
Alberto Griggio [Thu, 19 May 2005 13:11:06 +0000 (13:11 +0000)]
various optimizations (to paramodulation and passive clause selection)

19 years agocommented out some debugging messages
Stefano Zacchiroli [Thu, 19 May 2005 10:06:54 +0000 (10:06 +0000)]
commented out some debugging messages

19 years agoconnected instance to the web search engine
Stefano Zacchiroli [Thu, 19 May 2005 10:05:45 +0000 (10:05 +0000)]
connected instance to the web search engine

19 years agochanged debugging code which saves xml input document and input uri so
Stefano Zacchiroli [Thu, 19 May 2005 10:00:16 +0000 (10:00 +0000)]
changed debugging code which saves xml input document and input uri so
that it is automatically enabled with debugging

19 years ago- die on CTRL-C or init.d/... stop instead of resurrecting
Stefano Zacchiroli [Thu, 19 May 2005 09:39:51 +0000 (09:39 +0000)]
- die on CTRL-C or init.d/... stop instead of resurrecting
- added (commented) debugging code to save xml document

19 years agounified grammars and lexers in a single one
Stefano Zacchiroli [Thu, 19 May 2005 08:32:52 +0000 (08:32 +0000)]
unified grammars and lexers in a single one

19 years agofixed some macros, added test_abort.ma
Enrico Tassi [Wed, 18 May 2005 14:34:40 +0000 (14:34 +0000)]
fixed some macros, added test_abort.ma

19 years agosnapshot (implemented level 3 grammar)
Stefano Zacchiroli [Wed, 18 May 2005 13:11:50 +0000 (13:11 +0000)]
snapshot (implemented level 3 grammar)

19 years agofixed some TODO in content2pres
Enrico Tassi [Wed, 18 May 2005 12:11:37 +0000 (12:11 +0000)]
fixed some TODO in content2pres

19 years agosnapshot, notably:
Stefano Zacchiroli [Wed, 18 May 2005 10:53:29 +0000 (10:53 +0000)]
snapshot, notably:
- fixed some lexer bugs
- implemented level 2 patterns grammar

19 years agosnapshot, notably:
Stefano Zacchiroli [Tue, 17 May 2005 22:22:26 +0000 (22:22 +0000)]
snapshot, notably:
- solved factorization issues in level 1
- support for multiple grammars in cicNotationParser

19 years agosnapshot
Stefano Zacchiroli [Tue, 17 May 2005 22:14:49 +0000 (22:14 +0000)]
snapshot

19 years agofirst check-in of cic_notation
Stefano Zacchiroli [Tue, 17 May 2005 15:34:42 +0000 (15:34 +0000)]
first check-in of cic_notation

19 years agofixed whelp bar
Enrico Tassi [Tue, 17 May 2005 15:24:48 +0000 (15:24 +0000)]
fixed whelp bar

19 years agofixed Whelp stuff
Enrico Tassi [Tue, 17 May 2005 15:24:11 +0000 (15:24 +0000)]
fixed Whelp stuff

19 years agoaded comment
Enrico Tassi [Tue, 17 May 2005 15:23:23 +0000 (15:23 +0000)]
aded comment

19 years agocosmetic changes
Stefano Zacchiroli [Tue, 17 May 2005 13:08:22 +0000 (13:08 +0000)]
cosmetic changes

19 years agobugfix: avoid duplicate entries while indexing (changed implementation
Stefano Zacchiroli [Tue, 17 May 2005 13:08:11 +0000 (13:08 +0000)]
bugfix: avoid duplicate entries while indexing (changed implementation
so that sets are internally used everywhere instead of lists, which are
now used only for implementing API)

19 years ago- cathes more Mysql errors which could happen during post-indexing actions
Stefano Zacchiroli [Tue, 17 May 2005 13:05:38 +0000 (13:05 +0000)]
- cathes more Mysql errors which could happen during post-indexing actions
- bugfix in hits table handling during post-indexing actions
- added copyright info

19 years agobugfix in elim, cardinality constraint should >= 1 not > 1
Stefano Zacchiroli [Tue, 17 May 2005 13:03:34 +0000 (13:03 +0000)]
bugfix in elim, cardinality constraint should >= 1 not > 1

19 years ago- no longer needs PXP
Stefano Zacchiroli [Mon, 16 May 2005 16:03:13 +0000 (16:03 +0000)]
- no longer needs PXP
- added "interpolate" paramater to register iterators

19 years agoadded images
Enrico Tassi [Mon, 16 May 2005 15:24:20 +0000 (15:24 +0000)]
added images

19 years agoadded examples
Enrico Tassi [Mon, 16 May 2005 15:23:34 +0000 (15:23 +0000)]
added examples

19 years agoadded comments, fixed history, added loadList to browser
Enrico Tassi [Mon, 16 May 2005 15:23:07 +0000 (15:23 +0000)]
added comments, fixed history, added loadList to browser

19 years agosome hacks to make the sequent window pretty nice
Enrico Tassi [Mon, 16 May 2005 15:21:32 +0000 (15:21 +0000)]
some hacks to make the sequent window pretty nice

19 years agofixed instance
Enrico Tassi [Mon, 16 May 2005 15:21:00 +0000 (15:21 +0000)]
fixed instance

19 years agoadded comments
Enrico Tassi [Mon, 16 May 2005 15:20:34 +0000 (15:20 +0000)]
added comments

19 years agoadded saturation.opt to the ignore list
Alberto Griggio [Sun, 15 May 2005 12:10:57 +0000 (12:10 +0000)]
added saturation.opt to the ignore list

19 years agofixes (mainly) to demodulation and meta_convertibility
Alberto Griggio [Sun, 15 May 2005 12:08:59 +0000 (12:08 +0000)]
fixes (mainly) to demodulation and meta_convertibility

19 years agoadded support for hits table
Stefano Zacchiroli [Fri, 13 May 2005 13:01:25 +0000 (13:01 +0000)]
added support for hits table

19 years agoadded list and fill actions
Stefano Zacchiroli [Fri, 13 May 2005 13:01:12 +0000 (13:01 +0000)]
added list and fill actions

19 years agosync script among databases
Stefano Zacchiroli [Fri, 13 May 2005 13:00:59 +0000 (13:00 +0000)]
sync script among databases

19 years agosupport hits table
Stefano Zacchiroli [Fri, 13 May 2005 13:00:35 +0000 (13:00 +0000)]
support hits table

19 years agosql for filling hits table
Stefano Zacchiroli [Fri, 13 May 2005 11:22:06 +0000 (11:22 +0000)]
sql for filling hits table

19 years agoadded hits table
Stefano Zacchiroli [Fri, 13 May 2005 11:19:14 +0000 (11:19 +0000)]
added hits table

19 years agobetter table creator
Enrico Tassi [Fri, 13 May 2005 11:14:08 +0000 (11:14 +0000)]
better table creator

19 years agoadded "all" table meaning "act on all tables"
Stefano Zacchiroli [Fri, 13 May 2005 11:08:33 +0000 (11:08 +0000)]
added "all" table meaning "act on all tables"

19 years agofixed
Stefano Zacchiroli [Fri, 13 May 2005 11:07:33 +0000 (11:07 +0000)]
fixed

19 years agofix bad space
Enrico Tassi [Fri, 13 May 2005 10:58:53 +0000 (10:58 +0000)]
fix bad space

19 years agonow the extractor manager renames the tables (old tables are renamed to _BACKUP)
Enrico Tassi [Fri, 13 May 2005 10:58:40 +0000 (10:58 +0000)]
now the extractor manager renames the tables (old tables are renamed to _BACKUP)

19 years agosome more statements
Enrico Tassi [Fri, 13 May 2005 10:48:33 +0000 (10:48 +0000)]
some more statements

19 years agoadded index on refRel and the rename table statements
Enrico Tassi [Fri, 13 May 2005 10:20:20 +0000 (10:20 +0000)]
added index on refRel and the rename table statements

19 years ago- ported to new ocaml-http API
Stefano Zacchiroli [Fri, 13 May 2005 09:16:51 +0000 (09:16 +0000)]
- ported to new ocaml-http API
- uses Arg for cmdline parsing

19 years agoexported new_metasenv_for_apply, needed by the paramodulation stuff...
Alberto Griggio [Fri, 13 May 2005 09:15:33 +0000 (09:15 +0000)]
exported new_metasenv_for_apply, needed by the paramodulation stuff...

19 years agofixed demodulation bug
Alberto Griggio [Fri, 13 May 2005 09:08:30 +0000 (09:08 +0000)]
fixed demodulation bug

19 years agomoved string_of_equality into utils
Alberto Griggio [Fri, 13 May 2005 09:05:27 +0000 (09:05 +0000)]
moved string_of_equality into utils

19 years agofirst commit of paramodulation-based theorem proving for helm...
Alberto Griggio [Thu, 12 May 2005 17:02:22 +0000 (17:02 +0000)]
first commit of paramodulation-based theorem proving for helm...

19 years agofixed memory leak (workaround)
Enrico Tassi [Thu, 12 May 2005 09:20:48 +0000 (09:20 +0000)]
fixed memory leak (workaround)

19 years agofixed Makefile
Stefano Zacchiroli [Thu, 12 May 2005 09:10:17 +0000 (09:10 +0000)]
fixed Makefile

19 years agofixed a TODO comment (MUTCASE _is_ implemented)
Stefano Zacchiroli [Thu, 12 May 2005 09:07:27 +0000 (09:07 +0000)]
fixed a TODO comment (MUTCASE _is_ implemented)

19 years agohandling of variables with body
Stefano Zacchiroli [Thu, 12 May 2005 09:01:45 +0000 (09:01 +0000)]
handling of variables with body

19 years agohandle XmlPushParser.Parse_error exception
Stefano Zacchiroli [Wed, 11 May 2005 16:39:00 +0000 (16:39 +0000)]
handle XmlPushParser.Parse_error exception

19 years agoadded Parse_error exception and pretty printing of Expat errors
Stefano Zacchiroli [Wed, 11 May 2005 16:34:48 +0000 (16:34 +0000)]
added Parse_error exception and pretty printing of Expat errors

19 years agomore detailed info about peon's problems
Stefano Zacchiroli [Tue, 10 May 2005 15:55:43 +0000 (15:55 +0000)]
more detailed info about peon's problems

19 years agoignores test and test.opt
Stefano Zacchiroli [Tue, 10 May 2005 10:59:45 +0000 (10:59 +0000)]
ignores test and test.opt

19 years ago- changes defaults of getxml (format gzipped, don't patch dtd)
Stefano Zacchiroli [Tue, 10 May 2005 10:59:13 +0000 (10:59 +0000)]
- changes defaults of getxml (format gzipped, don't patch dtd)
- big bug fix which avoid spurious \n at end of gzipped file

19 years agomoved up xml, now needed by CicParser
Stefano Zacchiroli [Tue, 10 May 2005 10:58:28 +0000 (10:58 +0000)]
moved up xml, now needed by CicParser

19 years agomake use of gzipped type and body
Stefano Zacchiroli [Tue, 10 May 2005 10:58:05 +0000 (10:58 +0000)]
make use of gzipped type and body

19 years agomoved xmlPushParser in ocaml/xml/ since it does not depend on cic
Stefano Zacchiroli [Tue, 10 May 2005 10:57:26 +0000 (10:57 +0000)]
moved xmlPushParser in ocaml/xml/ since it does not depend on cic

19 years agomade optional dependency on thread library and compile time flag
Stefano Zacchiroli [Tue, 10 May 2005 10:56:45 +0000 (10:56 +0000)]
made optional dependency on thread library and compile time flag

19 years agoadded dep on expat
Stefano Zacchiroli [Tue, 10 May 2005 10:56:19 +0000 (10:56 +0000)]
added dep on expat

19 years agoocaml/ todo list
Stefano Zacchiroli [Tue, 10 May 2005 10:10:47 +0000 (10:10 +0000)]
ocaml/ todo list

19 years agomoved here xmlPushParser.ml and corresponding test
Stefano Zacchiroli [Tue, 10 May 2005 10:10:38 +0000 (10:10 +0000)]
moved here xmlPushParser.ml and corresponding test

19 years agoadded 'tags' target (which index both matita/ and ocaml/ above)
Stefano Zacchiroli [Tue, 10 May 2005 06:46:53 +0000 (06:46 +0000)]
added 'tags' target (which index both matita/ and ocaml/ above)

19 years agoThe README file was patched
Ferruccio Guidi [Fri, 6 May 2005 19:59:13 +0000 (19:59 +0000)]
The README file was patched

19 years agoToolbox: preliminary version
Ferruccio Guidi [Fri, 6 May 2005 18:21:16 +0000 (18:21 +0000)]
Toolbox: preliminary version

19 years agoadded syntax for rewrite (TODO no rewrite-in-Hyp syntax)
Enrico Tassi [Fri, 6 May 2005 10:13:16 +0000 (10:13 +0000)]
added syntax for rewrite (TODO no rewrite-in-Hyp syntax)
bold sequent line
more space between the sequent line and the formulae

19 years agofactorization of rewrite.
Enrico Tassi [Fri, 6 May 2005 10:12:16 +0000 (10:12 +0000)]
factorization of rewrite.
now the tactic also does a beta reduction step
(behaving as expected)

19 years ago- ported to new CicParser interface which requires an uri argument to be
Stefano Zacchiroli [Thu, 5 May 2005 15:55:37 +0000 (15:55 +0000)]
- ported to new CicParser interface which requires an uri argument to be
  passed to parsing functions
- removed orrible hack for sort parsing

19 years agoadded "tags" target to generate vim tags with otags
Stefano Zacchiroli [Thu, 5 May 2005 15:54:53 +0000 (15:54 +0000)]
added "tags" target to generate vim tags with otags

19 years agoadded test and test.opt targets
Stefano Zacchiroli [Thu, 5 May 2005 15:54:34 +0000 (15:54 +0000)]
added test and test.opt targets

19 years ago- implemented CicPushParser which parser CIC objects using Expat
Stefano Zacchiroli [Thu, 5 May 2005 15:54:14 +0000 (15:54 +0000)]
- implemented CicPushParser which parser CIC objects using Expat
  (currently, old PXP parser have been renamed to CicPxpParser, new one
  has been named CicPushParser and CicParser can includes one of the
  two. It includes CicPushParser per default)
- added mandatory uri parameter to main parsing functions, it is needed
  for creation of universes when Type sorts are encountered

19 years ago- added .cvsignore
Stefano Zacchiroli [Thu, 5 May 2005 15:35:16 +0000 (15:35 +0000)]
- added .cvsignore
- removed test.ml (which has been promoted to extractor.ml)

19 years agotest_instance.ma
Andrea Asperti [Thu, 5 May 2005 14:15:51 +0000 (14:15 +0000)]
test_instance.ma

19 years agoSome modifications due to instance.
Andrea Asperti [Thu, 5 May 2005 11:14:14 +0000 (11:14 +0000)]
Some modifications due to instance.

19 years agoadded .depend
Stefano Zacchiroli [Thu, 5 May 2005 08:02:57 +0000 (08:02 +0000)]
added .depend

19 years agoadded extractor_manager
Enrico Tassi [Wed, 4 May 2005 13:25:58 +0000 (13:25 +0000)]
added extractor_manager

19 years agoadded new extractor based on MetadataDb.index_obj
Enrico Tassi [Tue, 3 May 2005 17:12:49 +0000 (17:12 +0000)]
added new extractor based on MetadataDb.index_obj

19 years agosync with SqlStatements
Enrico Tassi [Tue, 3 May 2005 14:43:12 +0000 (14:43 +0000)]
sync with SqlStatements

19 years agoadded DROP statements to sqlStatements
Enrico Tassi [Tue, 3 May 2005 14:37:30 +0000 (14:37 +0000)]
added DROP statements to sqlStatements

19 years agomore friendly sqlStatements api
Enrico Tassi [Tue, 3 May 2005 13:55:07 +0000 (13:55 +0000)]
more friendly sqlStatements api

19 years agoadded examples
Enrico Tassi [Tue, 3 May 2005 13:40:53 +0000 (13:40 +0000)]
added examples

19 years agoadded table_creator (comman line frontend to SqlStatements)
Enrico Tassi [Tue, 3 May 2005 13:39:34 +0000 (13:39 +0000)]
added table_creator (comman line frontend to SqlStatements)

19 years agoadded sqlStatements module (contains all CREATE TABLE/INDEX)
Enrico Tassi [Tue, 3 May 2005 13:38:25 +0000 (13:38 +0000)]
added sqlStatements module (contains all CREATE TABLE/INDEX)

19 years agoadded instance
Enrico Tassi [Tue, 3 May 2005 12:50:34 +0000 (12:50 +0000)]
added instance

19 years agofix for instance
Enrico Tassi [Tue, 3 May 2005 12:50:12 +0000 (12:50 +0000)]
fix for instance

19 years agoFirst version of instance.
Andrea Asperti [Tue, 3 May 2005 12:01:36 +0000 (12:01 +0000)]
First version of instance.

19 years agoattached auto
Enrico Tassi [Mon, 2 May 2005 13:58:45 +0000 (13:58 +0000)]
attached auto

19 years agoattached auto
Enrico Tassi [Mon, 2 May 2005 13:47:30 +0000 (13:47 +0000)]
attached auto

19 years agoadded the count table
Enrico Tassi [Mon, 2 May 2005 12:55:02 +0000 (12:55 +0000)]
added the count table

19 years agoadded Match (partially) and sync with the count table
Enrico Tassi [Mon, 2 May 2005 12:53:56 +0000 (12:53 +0000)]
added Match (partially) and sync with the count table

19 years agoadded ast for Match
Enrico Tassi [Mon, 2 May 2005 12:52:59 +0000 (12:52 +0000)]
added ast for Match

19 years agoremoved no_inconcl_aux, no_concl_hyp, no_hyp and added count
Enrico Tassi [Mon, 2 May 2005 12:52:30 +0000 (12:52 +0000)]
removed no_inconcl_aux, no_concl_hyp, no_hyp and added count

19 years agoadded more assertions on universes when loaded from dump (and fixed some bugs concern...
Enrico Tassi [Fri, 29 Apr 2005 18:52:57 +0000 (18:52 +0000)]
added more assertions on universes when loaded from dump (and fixed some bugs concerning re-hash-consing)

19 years agoadded the orrible hack to the parser that is needed to call CicUniv.fresh() properly
Enrico Tassi [Fri, 29 Apr 2005 18:52:08 +0000 (18:52 +0000)]
added the orrible hack to the parser that is needed to call CicUniv.fresh() properly

19 years agohint -> experimental_hint
Enrico Tassi [Fri, 29 Apr 2005 13:45:41 +0000 (13:45 +0000)]
hint -> experimental_hint