]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agofix
Enrico Tassi [Wed, 25 May 2005 14:02:20 +0000 (14:02 +0000)]
fix

19 years agofix
Enrico Tassi [Wed, 25 May 2005 13:46:11 +0000 (13:46 +0000)]
fix

19 years agoapply now tries both to reduce and to not reduce the applied term
Enrico Tassi [Wed, 25 May 2005 13:45:21 +0000 (13:45 +0000)]
apply now tries both to reduce and to not reduce the applied term

19 years ago\lambda x.x y ----> \lambda x.(x y)
Enrico Tassi [Wed, 25 May 2005 13:44:34 +0000 (13:44 +0000)]
\lambda x.x y ----> \lambda x.(x y)

19 years agosnapshot
Stefano Zacchiroli [Wed, 25 May 2005 09:49:50 +0000 (09:49 +0000)]
snapshot
- implemented first draft of extensible parser ... brrrrrr

19 years agoclean typo
Stefano Zacchiroli [Tue, 24 May 2005 15:42:20 +0000 (15:42 +0000)]
clean typo

19 years agoreverted to ==
Enrico Tassi [Tue, 24 May 2005 14:54:47 +0000 (14:54 +0000)]
reverted to ==

19 years agoadded .theory check
Enrico Tassi [Tue, 24 May 2005 14:15:06 +0000 (14:15 +0000)]
added .theory check

19 years agofixed missing -syntax when using ocamlopt
Enrico Tassi [Tue, 24 May 2005 14:14:28 +0000 (14:14 +0000)]
fixed missing -syntax when using ocamlopt

19 years agofixed precedence of \to
Enrico Tassi [Tue, 24 May 2005 13:57:35 +0000 (13:57 +0000)]
fixed precedence of \to

19 years agoadded simpl test script
Enrico Tassi [Tue, 24 May 2005 13:34:02 +0000 (13:34 +0000)]
added simpl test script

19 years agoadded simpl
Enrico Tassi [Tue, 24 May 2005 13:33:48 +0000 (13:33 +0000)]
added simpl

19 years agofixed syntax
Enrico Tassi [Tue, 24 May 2005 13:33:35 +0000 (13:33 +0000)]
fixed syntax

19 years agonew simpl semantic (now = and not == since you can't write a pointer to a script)
Enrico Tassi [Tue, 24 May 2005 13:33:02 +0000 (13:33 +0000)]
new simpl semantic (now = and not == since you can't write a pointer to a script)

19 years agoadded lost elim_intros_tac
Enrico Tassi [Tue, 24 May 2005 10:36:52 +0000 (10:36 +0000)]
added lost elim_intros_tac

19 years agofix
Andrea Asperti [Tue, 24 May 2005 10:09:08 +0000 (10:09 +0000)]
fix

19 years agoAdded a new tactic elim_intros (without simpl of the new goal).
Andrea Asperti [Tue, 24 May 2005 08:33:06 +0000 (08:33 +0000)]
Added a new tactic elim_intros (without simpl of the new goal).

19 years agoelim -> elim_intros (no simpl)
Andrea Asperti [Tue, 24 May 2005 08:31:13 +0000 (08:31 +0000)]
elim -> elim_intros (no simpl)

19 years agoAdded sql/drop_mowgli_tables.mysql.sql
Claudio Sacerdoti Coen [Mon, 23 May 2005 15:59:30 +0000 (15:59 +0000)]
Added sql/drop_mowgli_tables.mysql.sql

19 years agoadded rule to generate camlp4 expansion of cicNotationParser.ml (in order
Stefano Zacchiroli [Mon, 23 May 2005 15:23:38 +0000 (15:23 +0000)]
added rule to generate camlp4 expansion of cicNotationParser.ml (in order
to reverse engineer Grammar.extend usage ...)

19 years agosnapshot
Stefano Zacchiroli [Mon, 23 May 2005 15:18:20 +0000 (15:18 +0000)]
snapshot

19 years agosnapshot
Stefano Zacchiroli [Mon, 23 May 2005 13:07:32 +0000 (13:07 +0000)]
snapshot
- added parse tree for all levels
- implemented parse tree construction for level 1 and 2

19 years agofixed clean that wasn't returning the right list of uris owned by the user
Enrico Tassi [Mon, 23 May 2005 11:53:08 +0000 (11:53 +0000)]
fixed clean that wasn't returning the right list of uris owned by the user

19 years agoadded qed
Enrico Tassi [Mon, 23 May 2005 11:28:55 +0000 (11:28 +0000)]
added qed

19 years agoAdded andrea.ma
Andrea Asperti [Mon, 23 May 2005 11:18:45 +0000 (11:18 +0000)]
Added andrea.ma

19 years agoswitched to cdbs for debian/rules (now 2 lines long!!!!)
Stefano Zacchiroli [Sun, 22 May 2005 22:03:18 +0000 (22:03 +0000)]
switched to cdbs for debian/rules (now 2 lines long!!!!)

19 years agoWhen we unify a Prod against a term t2 which is not a Prod we
Andrea Asperti [Fri, 20 May 2005 15:26:55 +0000 (15:26 +0000)]
When we unify a Prod against a term t2 which is not a Prod we
now try a whd of t2.

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