]>
matita.cs.unibo.it Git - helm.git/log
Enrico Tassi [Sun, 18 Jun 2006 12:17:18 +0000 (12:17 +0000)]
- some fixes regarding URIs of equality that now should be coherent with the
one of the goal
- eliminated the stack overflow issue when building the proof
Enrico Tassi [Sun, 18 Jun 2006 12:08:58 +0000 (12:08 +0000)]
instead of including library_notation we include logic/equality that is smaller
Enrico Tassi [Sun, 18 Jun 2006 10:49:22 +0000 (10:49 +0000)]
fix
Ferruccio Guidi [Fri, 16 Jun 2006 20:45:00 +0000 (20:45 +0000)]
contribution on relational arithmetics started
Enrico Tassi [Fri, 16 Jun 2006 19:07:08 +0000 (19:07 +0000)]
fixed
Enrico Tassi [Fri, 16 Jun 2006 18:51:18 +0000 (18:51 +0000)]
fixes
Enrico Tassi [Fri, 16 Jun 2006 16:06:41 +0000 (16:06 +0000)]
ecco le gatte da pelare
Enrico Tassi [Fri, 16 Jun 2006 11:51:08 +0000 (11:51 +0000)]
ancient bug solved. if the term is (eq TY A B) the signature of A and B was
ignored if TY was a Sort.
Enrico Tassi [Fri, 16 Jun 2006 11:47:25 +0000 (11:47 +0000)]
some more on equalities
Enrico Tassi [Fri, 16 Jun 2006 09:03:24 +0000 (09:03 +0000)]
added log.120.orsay.txt and comparison
Andrea Asperti [Thu, 15 Jun 2006 09:39:55 +0000 (09:39 +0000)]
some examples of the new ApplyS tactic
Andrea Asperti [Thu, 15 Jun 2006 09:39:20 +0000 (09:39 +0000)]
examples of applyS
Andrea Asperti [Thu, 15 Jun 2006 09:38:42 +0000 (09:38 +0000)]
Apply-Silvie tactic added!
Andrea Asperti [Thu, 15 Jun 2006 09:38:08 +0000 (09:38 +0000)]
added applyS
Andrea Asperti [Thu, 15 Jun 2006 09:37:49 +0000 (09:37 +0000)]
some fixed done in Orsay:
- supL is called on both sides if the equation is not oriented
- contextualize_rewrites fixed if multiple equalities are used (equalities on different types)
Andrea Asperti [Thu, 15 Jun 2006 09:35:47 +0000 (09:35 +0000)]
exported 2 functions needed by applyS
Andrea Asperti [Thu, 15 Jun 2006 09:24:46 +0000 (09:24 +0000)]
...
Andrea Asperti [Thu, 15 Jun 2006 09:22:29 +0000 (09:22 +0000)]
default constants are now the matita standard library ones and not the one from Coq.
the makefile should work on every checkout, since the path for the TPTP stuff is not hardcoded, but ppoint to the TPTP-VERSION/ directory in the user's home.
Stefano Zacchiroli [Wed, 14 Jun 2006 15:04:13 +0000 (15:04 +0000)]
bumped date
Stefano Zacchiroli [Wed, 14 Jun 2006 15:03:46 +0000 (15:03 +0000)]
better wording of a sentence
Stefano Zacchiroli [Wed, 14 Jun 2006 14:41:44 +0000 (14:41 +0000)]
center figures in HTML version of the manual using CSS
Stefano Zacchiroli [Wed, 14 Jun 2006 14:40:06 +0000 (14:40 +0000)]
changed install target so that figures are instaled as well
Stefano Zacchiroli [Wed, 14 Jun 2006 14:33:57 +0000 (14:33 +0000)]
fixed bad spellend "stantard"
Stefano Zacchiroli [Wed, 14 Jun 2006 14:33:23 +0000 (14:33 +0000)]
removed old ignore lines about matita.conf.xml.ROLE
Stefano Zacchiroli [Wed, 14 Jun 2006 14:32:46 +0000 (14:32 +0000)]
Enrico: bugfix, remove depend.errors upon destroy
Stefano Zacchiroli [Wed, 14 Jun 2006 14:30:32 +0000 (14:30 +0000)]
removed old debugging print
Enrico Tassi [Wed, 14 Jun 2006 14:14:11 +0000 (14:14 +0000)]
relocation of developments.png
Enrico Tassi [Wed, 14 Jun 2006 14:08:28 +0000 (14:08 +0000)]
adding the developments screenshot
Stefano Zacchiroli [Wed, 14 Jun 2006 08:51:33 +0000 (08:51 +0000)]
cosmetic: better placement of news box
Stefano Zacchiroli [Wed, 14 Jun 2006 08:49:31 +0000 (08:49 +0000)]
- added news section
- added <a name ...> on each level 2 heading
Stefano Zacchiroli [Wed, 14 Jun 2006 08:46:06 +0000 (08:46 +0000)]
added mention of the two mailing lists we have
Stefano Zacchiroli [Tue, 13 Jun 2006 14:39:41 +0000 (14:39 +0000)]
download.shtml is now valid xhtml 1.0 strict
Stefano Zacchiroli [Tue, 13 Jun 2006 14:24:25 +0000 (14:24 +0000)]
bumped date
Stefano Zacchiroli [Tue, 13 Jun 2006 14:23:09 +0000 (14:23 +0000)]
new path for XSLT sytlesheets
Stefano Zacchiroli [Tue, 13 Jun 2006 14:22:43 +0000 (14:22 +0000)]
typo: titleabbrev stuff should not be bold
Stefano Zacchiroli [Tue, 13 Jun 2006 14:18:33 +0000 (14:18 +0000)]
added generation of quick reference card of tactic syntax
Stefano Zacchiroli [Tue, 13 Jun 2006 12:03:51 +0000 (12:03 +0000)]
- distributed matitaGeneratedGui.ml (needed)
- when distributed 'world' is the default target
Stefano Zacchiroli [Tue, 13 Jun 2006 11:42:28 +0000 (11:42 +0000)]
generate gui code upon distribution
Stefano Zacchiroli [Tue, 13 Jun 2006 10:21:57 +0000 (10:21 +0000)]
distribute more stuff
added an install target to the manual makefile
Stefano Zacchiroli [Tue, 13 Jun 2006 10:21:28 +0000 (10:21 +0000)]
reordered author list
Stefano Zacchiroli [Tue, 13 Jun 2006 10:19:57 +0000 (10:19 +0000)]
use the install target of the manual
Stefano Zacchiroli [Tue, 13 Jun 2006 10:00:50 +0000 (10:00 +0000)]
updated some distributed stuff
Stefano Zacchiroli [Tue, 13 Jun 2006 09:54:21 +0000 (09:54 +0000)]
recursive invocation of distr_pre
Stefano Zacchiroli [Tue, 13 Jun 2006 09:53:27 +0000 (09:53 +0000)]
filled README, BUGS, and other files useful for the distribution
Stefano Zacchiroli [Tue, 13 Jun 2006 08:33:55 +0000 (08:33 +0000)]
moved benchmnarks/ dir outside of components/
Stefano Zacchiroli [Tue, 13 Jun 2006 08:14:39 +0000 (08:14 +0000)]
aligned matita logo to the left
Stefano Zacchiroli [Mon, 12 Jun 2006 11:36:36 +0000 (11:36 +0000)]
added shortcut targets
Stefano Zacchiroli [Mon, 12 Jun 2006 11:27:15 +0000 (11:27 +0000)]
added dummy <entry /> to make yelp happy
Stefano Zacchiroli [Mon, 12 Jun 2006 11:22:00 +0000 (11:22 +0000)]
- better formatting/factorization of tables used for grammar description
- improved rendering toward TeX
Ferruccio Guidi [Sun, 11 Jun 2006 08:16:13 +0000 (08:16 +0000)]
fix in the development page
Ferruccio Guidi [Sun, 11 Jun 2006 08:13:05 +0000 (08:13 +0000)]
- slight fix in lapply syntax
- Ferruccio Guidi is NOT a former member :)
Stefano Zacchiroli [Sat, 10 Jun 2006 17:06:57 +0000 (17:06 +0000)]
added support for displaying the list of papers related to matita in the documentation page (currently commented out)
Stefano Zacchiroli [Sat, 10 Jun 2006 17:06:26 +0000 (17:06 +0000)]
added reference to the online version of the manual
Stefano Zacchiroli [Sat, 10 Jun 2006 16:27:17 +0000 (16:27 +0000)]
added deps, create target dir if missing
Stefano Zacchiroli [Sat, 10 Jun 2006 16:26:55 +0000 (16:26 +0000)]
ignore generated stuff
Stefano Zacchiroli [Sat, 10 Jun 2006 16:26:33 +0000 (16:26 +0000)]
tiny version of the logo
Stefano Zacchiroli [Sat, 10 Jun 2006 16:25:50 +0000 (16:25 +0000)]
keeping the generated manual on svn is overkilling
Stefano Zacchiroli [Sat, 10 Jun 2006 16:24:25 +0000 (16:24 +0000)]
generate deps on the fly
added dep on the stylesheets
Stefano Zacchiroli [Sat, 10 Jun 2006 16:24:03 +0000 (16:24 +0000)]
removed overkilling info for our manual
Stefano Zacchiroli [Sat, 10 Jun 2006 16:21:25 +0000 (16:21 +0000)]
consistent naming of the calculus
Stefano Zacchiroli [Sat, 10 Jun 2006 16:20:58 +0000 (16:20 +0000)]
css stylesheets for the on-line manual
Stefano Zacchiroli [Sat, 10 Jun 2006 16:20:44 +0000 (16:20 +0000)]
factorized legal stuff like other chapters
Stefano Zacchiroli [Sat, 10 Jun 2006 16:20:16 +0000 (16:20 +0000)]
manual regenerated
Ferruccio Guidi [Sat, 10 Jun 2006 14:44:43 +0000 (14:44 +0000)]
new documentation for the decompose tactic
Stefano Zacchiroli [Sat, 10 Jun 2006 13:20:50 +0000 (13:20 +0000)]
first generation of manual from docbook
better Makefile
Stefano Zacchiroli [Sat, 10 Jun 2006 13:17:48 +0000 (13:17 +0000)]
added automatic generation of the manual
Stefano Zacchiroli [Sat, 10 Jun 2006 11:37:11 +0000 (11:37 +0000)]
yet another screenshot
Stefano Zacchiroli [Sat, 10 Jun 2006 11:29:39 +0000 (11:29 +0000)]
added screenshots describing matita features
Stefano Zacchiroli [Sat, 10 Jun 2006 09:15:15 +0000 (09:15 +0000)]
- all final shtml are now well formed XML documents
- added a link to the logo in the top left corner
- structured and commented the CSS stylesheet
- added $Id$ where missing
- the Makefile no longer builds images when invoked with no targets
Stefano Zacchiroli [Fri, 9 Jun 2006 23:59:27 +0000 (23:59 +0000)]
wording
Stefano Zacchiroli [Fri, 9 Jun 2006 23:52:36 +0000 (23:52 +0000)]
- added a real-life index page
- removed the label 'matita' on the top-left logo
- added a big 'matita' label for the index page
- factorized common stuff that goes inside <head> in a new SSI
Stefano Zacchiroli [Fri, 9 Jun 2006 19:50:21 +0000 (19:50 +0000)]
rewored website layout and internal structure:
- moved menu bar to the left
- added logo on the top left
- added headings
Stefano Zacchiroli [Fri, 9 Jun 2006 16:16:02 +0000 (16:16 +0000)]
scaled down
Stefano Zacchiroli [Fri, 9 Jun 2006 16:12:28 +0000 (16:12 +0000)]
scaled down
Stefano Zacchiroli [Fri, 9 Jun 2006 16:03:44 +0000 (16:03 +0000)]
added small version of the matita logo
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 15:54:19 +0000 (15:54 +0000)]
More documentation committed.
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 15:44:07 +0000 (15:44 +0000)]
Syntactic bug changed: t in "unfold t" must be a tactic_term, not a term
Stefano Zacchiroli [Fri, 9 Jun 2006 15:12:20 +0000 (15:12 +0000)]
reworked css and html structure, continuing offline ...
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 15:00:58 +0000 (15:00 +0000)]
Tactics are now documented using bolds for terminal symbols.
Stefano Zacchiroli [Fri, 9 Jun 2006 14:39:58 +0000 (14:39 +0000)]
moved matita-bugs.ong -> matita-medium.png
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 14:39:14 +0000 (14:39 +0000)]
1. the default for the default equality/absurd/true/false URIs used to be
the Coq ones; now it is None
2. legacy/coq.ma changed to set the default URIs for Coq
3. generation of inversion principles is now branched again
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 14:37:20 +0000 (14:37 +0000)]
[a-z] syntax documented
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 14:33:16 +0000 (14:33 +0000)]
Lexical conventions documented.
Stefano Zacchiroli [Fri, 9 Jun 2006 14:31:34 +0000 (14:31 +0000)]
added css and image for bugzilla
Andrea Asperti [Fri, 9 Jun 2006 13:14:11 +0000 (13:14 +0000)]
Notation for congruent.
Restyling of fermat's little theorem with tynicals.
Stefano Zacchiroli [Thu, 8 Jun 2006 16:24:52 +0000 (16:24 +0000)]
the Matita manual is now convertible to a decent .tex that is processable both
by latex and pdflatex, changes involved:
- use the 'unicode' latex package. The unicode package, being quite large, has
been imported under trunk/software/share/texmf/unicode
- added the definition of mappings from some unicode symbol we use (and which
are not defined in the default unicode package) to tex macros. See
share/texmf/unicode/config/matita.ucf
- added some parameters to the stylesheet used to generate .tex from .xml
Enrico Tassi [Thu, 8 Jun 2006 12:00:35 +0000 (12:00 +0000)]
developments added
Stefano Zacchiroli [Wed, 7 Jun 2006 16:38:34 +0000 (16:38 +0000)]
added "dumb" test target
Stefano Zacchiroli [Wed, 7 Jun 2006 14:50:33 +0000 (14:50 +0000)]
Attempt to make our markup respect the docbook specification(!), major changes
required:
1) added <para> wrappers where missing
2) added titles to tables
3) removed empty <thead> elements
Point (3) make yelp now shows rules in tables used for syntax references. IMO
this not a good reason to have empty <thead> elements, since they violates the
docbook DTDs. Either yelp should be fixed to not ignore frame/rowsep/colsep
attributes (as it currently does) or we need to find a different markup for
displaying EBNF like grammars.
Stefano Zacchiroli [Mon, 5 Jun 2006 11:38:24 +0000 (11:38 +0000)]
bug fixed in doc
Claudio Sacerdoti Coen [Mon, 5 Jun 2006 11:27:13 +0000 (11:27 +0000)]
(co)inductive type declarations are now documented
Claudio Sacerdoti Coen [Mon, 5 Jun 2006 11:08:49 +0000 (11:08 +0000)]
Record syntax is now described.
More &TODO; put here and there.
Stefano Zacchiroli [Thu, 1 Jun 2006 15:32:34 +0000 (15:32 +0000)]
implemented tinycals:
- 1,2,3: ...
- *:
Stefano Zacchiroli [Thu, 1 Jun 2006 15:27:50 +0000 (15:27 +0000)]
commented the finally function
Enrico Tassi [Thu, 1 Jun 2006 13:28:19 +0000 (13:28 +0000)]
fix
Enrico Tassi [Thu, 1 Jun 2006 11:36:50 +0000 (11:36 +0000)]
...
Enrico Tassi [Thu, 1 Jun 2006 11:23:51 +0000 (11:23 +0000)]
...
Stefano Zacchiroli [Thu, 1 Jun 2006 10:52:11 +0000 (10:52 +0000)]
use the appropriate chain of transormations for pretty printing term
Stefano Zacchiroli [Thu, 1 Jun 2006 10:51:34 +0000 (10:51 +0000)]
made pp_term parametric and explained the proper way of solving the object pretty printing problem
Claudio Sacerdoti Coen [Thu, 1 Jun 2006 09:57:50 +0000 (09:57 +0000)]
Bug fixed that made theory rendering bugged after visiting a whelp search page.