]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agomore verbose case failure message
Andrea Asperti [Tue, 31 May 2005 09:42:30 +0000 (09:42 +0000)]
more verbose case failure message

19 years agoadded chronometer
Andrea Asperti [Tue, 31 May 2005 09:40:51 +0000 (09:40 +0000)]
added chronometer

19 years agoadded automathic aliases for _ind _rec and _rect when generated
Andrea Asperti [Tue, 31 May 2005 09:40:36 +0000 (09:40 +0000)]
added automathic aliases for _ind _rec and _rect when generated

19 years agofix
Andrea Asperti [Tue, 31 May 2005 09:40:15 +0000 (09:40 +0000)]
fix

19 years agoadded automathic aliases for qed and definition
Enrico Tassi [Tue, 31 May 2005 08:40:54 +0000 (08:40 +0000)]
added automathic aliases for qed and definition

19 years agoadded shortcuts
Enrico Tassi [Tue, 31 May 2005 08:27:21 +0000 (08:27 +0000)]
added shortcuts

19 years agofix
Enrico Tassi [Tue, 31 May 2005 08:20:54 +0000 (08:20 +0000)]
fix

19 years agoadded uri_of_term
Stefano Zacchiroli [Mon, 30 May 2005 17:14:34 +0000 (17:14 +0000)]
added uri_of_term

19 years agomah...matita.ml
Enrico Tassi [Mon, 30 May 2005 16:03:57 +0000 (16:03 +0000)]
mah...matita.ml

19 years agofix
Andrea Asperti [Mon, 30 May 2005 15:57:28 +0000 (15:57 +0000)]
fix

19 years agoadded intros n
Andrea Asperti [Mon, 30 May 2005 15:57:07 +0000 (15:57 +0000)]
added intros n

19 years agoadded intros n.
Andrea Asperti [Mon, 30 May 2005 15:56:15 +0000 (15:56 +0000)]
added intros n.

19 years agoadded automathic aliases.
Andrea Asperti [Mon, 30 May 2005 11:40:00 +0000 (11:40 +0000)]
added automathic aliases.

19 years ago- commented out no longer needed macros Redo, Undo, Abort
Stefano Zacchiroli [Fri, 27 May 2005 16:54:05 +0000 (16:54 +0000)]
- commented out no longer needed macros Redo, Undo, Abort
- bugfix: correctly handles "cic:" and "cic:/" pseudo-uris in cicBrowser
- bugfix: fixed String.sub error on directories shorted than 5 chars

19 years agofixed otags invocation
Stefano Zacchiroli [Fri, 27 May 2005 16:52:58 +0000 (16:52 +0000)]
fixed otags invocation

19 years agocommented out no longer needed macros Redo, Undo, Abort
Stefano Zacchiroli [Fri, 27 May 2005 16:52:40 +0000 (16:52 +0000)]
commented out no longer needed macros Redo, Undo, Abort

19 years agoadded %.annot rule to create type annotation files
Stefano Zacchiroli [Fri, 27 May 2005 16:52:19 +0000 (16:52 +0000)]
added %.annot rule to create type annotation files

19 years agoremoved debug prerr_endline
Enrico Tassi [Fri, 27 May 2005 16:31:47 +0000 (16:31 +0000)]
removed debug prerr_endline

19 years agofixed matitac
Enrico Tassi [Fri, 27 May 2005 16:31:18 +0000 (16:31 +0000)]
fixed matitac

19 years agorefactored modules structure
Stefano Zacchiroli [Fri, 27 May 2005 15:23:19 +0000 (15:23 +0000)]
refactored modules structure

19 years ago* fold left/right implemented
Stefano Zacchiroli [Fri, 27 May 2005 14:59:40 +0000 (14:59 +0000)]
* fold left/right implemented

19 years agosnapshot
Stefano Zacchiroli [Fri, 27 May 2005 13:20:05 +0000 (13:20 +0000)]
snapshot
- first version with working DEFAULT magic

19 years ago1. removed obsolete comments
Andrea Asperti [Fri, 27 May 2005 11:01:16 +0000 (11:01 +0000)]
1. removed obsolete comments
2. extended delift to the case of meta in head position
3. added a cases (? t1) vs t2: ? gets unified to the beta
expansion of t2 w.r.t t1.

19 years agoNow the links to 7 pages at a time are shown. Cool.
Claudio Sacerdoti Coen [Thu, 26 May 2005 16:04:05 +0000 (16:04 +0000)]
Now the links to 7 pages at a time are shown. Cool.

19 years ago256 chars max ==> 1024 chars max (because of Coq)
Claudio Sacerdoti Coen [Thu, 26 May 2005 14:52:51 +0000 (14:52 +0000)]
256 chars max ==> 1024 chars max (because of Coq)

19 years agofixed issue with explicit named substitutions
Stefano Zacchiroli [Thu, 26 May 2005 14:13:23 +0000 (14:13 +0000)]
fixed issue with explicit named substitutions

19 years agoBugs fixed:
Claudio Sacerdoti Coen [Thu, 26 May 2005 13:10:32 +0000 (13:10 +0000)]
Bugs fixed:
 1. elim did not accept identifiers with "'" in the middle
 2. elim did not accpet URIs

19 years agosnapshot
Stefano Zacchiroli [Thu, 26 May 2005 11:42:22 +0000 (11:42 +0000)]
snapshot
- first commit with working list syntax

19 years agomultiple bindings inside OPT supported
Stefano Zacchiroli [Wed, 25 May 2005 16:41:30 +0000 (16:41 +0000)]
multiple bindings inside OPT supported

19 years agobugfix: "match" now works also when no type is provided for the matched term
Stefano Zacchiroli [Wed, 25 May 2005 15:13:21 +0000 (15:13 +0000)]
bugfix: "match" now works also when no type is provided for the matched term

19 years agolet rec example
Stefano Zacchiroli [Wed, 25 May 2005 15:11:59 +0000 (15:11 +0000)]
let rec example

19 years agosnapshot (first version in which some extensions work, e.g. infix +)
Stefano Zacchiroli [Wed, 25 May 2005 14:32:40 +0000 (14:32 +0000)]
snapshot (first version in which some extensions work, e.g. infix +)
ueeeeeehh!

19 years agosome work for Gares
Ferruccio Guidi [Wed, 25 May 2005 14:16:53 +0000 (14:16 +0000)]
some work for Gares

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