]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

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)