]>
matita.cs.unibo.it Git - helm.git/log
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
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
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
Stefano Zacchiroli [Fri, 9 Jun 2006 19:50:21 +0000 (19:50 +0000)]
rewored website layout and internal structure:
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
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.
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
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.
Stefano Zacchiroli [Thu, 1 Jun 2006 15:32:34 +0000 (15:32 +0000)]
implemented tinycals:
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.
Stefano Zacchiroli [Thu, 1 Jun 2006 09:32:12 +0000 (09:32 +0000)]
bugfix: rely on byte count instead of mixing byte and character count
Andrea Asperti [Thu, 1 Jun 2006 07:31:25 +0000 (07:31 +0000)]
Subsumption_subst must be applied to the initial proof before passing
Claudio Sacerdoti Coen [Wed, 31 May 2006 17:12:12 +0000 (17:12 +0000)]
Sigma algebras and measurable maps defined.
Claudio Sacerdoti Coen [Wed, 31 May 2006 15:54:25 +0000 (15:54 +0000)]
Committed a first experiment in the formalization of Lebesgue dominated
Enrico Tassi [Wed, 31 May 2006 13:54:57 +0000 (13:54 +0000)]
\n restored
Enrico Tassi [Wed, 31 May 2006 13:54:36 +0000 (13:54 +0000)]
fixed proofs, contextualization should now work.
Claudio Sacerdoti Coen [Tue, 30 May 2006 16:50:33 +0000 (16:50 +0000)]
1. the default encoding for the stylesheets is now UTF8
Claudio Sacerdoti Coen [Tue, 30 May 2006 15:48:33 +0000 (15:48 +0000)]
NuPRL stylesheets default encoding changed to UTF8
Claudio Sacerdoti Coen [Tue, 30 May 2006 14:56:58 +0000 (14:56 +0000)]
matita.txt updated
Claudio Sacerdoti Coen [Tue, 30 May 2006 14:30:19 +0000 (14:30 +0000)]
Bug fixed: theories were handled as base uris, not as uris of files.
Enrico Tassi [Tue, 30 May 2006 11:50:51 +0000 (11:50 +0000)]
letin are now sorted properly.
Enrico Tassi [Tue, 30 May 2006 10:44:55 +0000 (10:44 +0000)]
fixed proof generation again
Claudio Sacerdoti Coen [Tue, 30 May 2006 10:33:42 +0000 (10:33 +0000)]
use the proper top level function to parse terms
Claudio Sacerdoti Coen [Tue, 30 May 2006 10:22:57 +0000 (10:22 +0000)]
ZACK: export a top level function for parsing terms, it can't be bypassed due to the Obj.magic trick
Enrico Tassi [Tue, 30 May 2006 09:26:15 +0000 (09:26 +0000)]
...
Enrico Tassi [Tue, 30 May 2006 09:19:14 +0000 (09:19 +0000)]
A -> Univ
Enrico Tassi [Tue, 30 May 2006 09:09:37 +0000 (09:09 +0000)]
canonical and contextualize_rewrites are back, they seem to work now...
Enrico Tassi [Tue, 30 May 2006 08:59:27 +0000 (08:59 +0000)]
the function to create on the fly a symmetry step has been moved to equality
Enrico Tassi [Tue, 30 May 2006 08:42:24 +0000 (08:42 +0000)]
added our poor results to CASC 2005
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:14:33 +0000 (08:14 +0000)]
ZACK: ported to the latest ocaml-http API
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:13:55 +0000 (08:13 +0000)]
ZACK: ported to the latest ocaml-http API
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:11:37 +0000 (08:11 +0000)]
ported to the latest ocaml-http API
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:10:47 +0000 (08:10 +0000)]
ZACK: ported to the latest ocaml-http API
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:04:50 +0000 (08:04 +0000)]
ported to the latest ocaml-http API
Stefano Zacchiroli [Tue, 30 May 2006 07:58:45 +0000 (07:58 +0000)]
bugfix: when creating a daemon spec _use_ the auto_close value passed as argument instead of ignoring it
Stefano Zacchiroli [Mon, 29 May 2006 20:52:22 +0000 (20:52 +0000)]
- removed Http_daemon.{start,start\}
Enrico Tassi [Mon, 29 May 2006 20:44:57 +0000 (20:44 +0000)]
added some logs
Enrico Tassi [Mon, 29 May 2006 20:41:16 +0000 (20:41 +0000)]
fix
Enrico Tassi [Mon, 29 May 2006 20:40:35 +0000 (20:40 +0000)]
committed the base utils for TPTP processing
Stefano Zacchiroli [Mon, 29 May 2006 20:33:30 +0000 (20:33 +0000)]
added finally function
Enrico Tassi [Mon, 29 May 2006 20:32:58 +0000 (20:32 +0000)]
profilings are printed
Enrico Tassi [Mon, 29 May 2006 20:29:21 +0000 (20:29 +0000)]
- proofs by subsumption now add a symmetry step if needed
Stefano Zacchiroli [Mon, 29 May 2006 20:27:57 +0000 (20:27 +0000)]
forces bash as Makefile SHELL
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:36:36 +0000 (17:36 +0000)]
ensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:34:16 +0000 (17:34 +0000)]
lowered debugging level
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:24:43 +0000 (17:24 +0000)]
ensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:20:16 +0000 (17:20 +0000)]
OCAMLPATH is not overrid if already defined
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:13:03 +0000 (17:13 +0000)]
ensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:10:14 +0000 (17:10 +0000)]
ensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:03:24 +0000 (17:03 +0000)]
bugfix:
Claudio Sacerdoti Coen [Mon, 29 May 2006 16:54:47 +0000 (16:54 +0000)]
ensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 16:54:36 +0000 (16:54 +0000)]
ensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 14:12:40 +0000 (14:12 +0000)]
bug fix: use an (un)marshaller for get_opt instead of a getter
Stefano Zacchiroli [Mon, 29 May 2006 13:49:53 +0000 (13:49 +0000)]
OCAMLPATH is no longer overrid if already set in current environment
Claudio Sacerdoti Coen [Mon, 29 May 2006 13:41:52 +0000 (13:41 +0000)]
Bug fixed in fresh_name_generator: the function used to fail on beta redexes. Fixed trivially without
Stefano Zacchiroli [Mon, 29 May 2006 11:56:28 +0000 (11:56 +0000)]
added (TODO) section on tacticals)
Enrico Tassi [Sun, 28 May 2006 16:10:26 +0000 (16:10 +0000)]
weak equality on meta used when replacing.
Enrico Tassi [Sun, 28 May 2006 16:09:00 +0000 (16:09 +0000)]
added the rule field to goal_proof.
Enrico Tassi [Sun, 28 May 2006 16:07:33 +0000 (16:07 +0000)]
- fixed a bug in unification (not sure in the right way)
Claudio Sacerdoti Coen [Fri, 26 May 2006 15:58:47 +0000 (15:58 +0000)]
CALS tables enriched to make (crappy) docbook stylesheets happy.
Claudio Sacerdoti Coen [Fri, 26 May 2006 15:39:29 +0000 (15:39 +0000)]
Documentation fixed.
Claudio Sacerdoti Coen [Fri, 26 May 2006 15:14:41 +0000 (15:14 +0000)]
New documentation.
Claudio Sacerdoti Coen [Fri, 26 May 2006 14:18:09 +0000 (14:18 +0000)]
More documentation.
Claudio Sacerdoti Coen [Fri, 26 May 2006 13:41:55 +0000 (13:41 +0000)]
More documentation.
Claudio Sacerdoti Coen [Fri, 26 May 2006 12:46:32 +0000 (12:46 +0000)]
Recently introduced bug in CicRefine.eat_prods fixed: a whd was now missing.
Claudio Sacerdoti Coen [Fri, 26 May 2006 12:38:42 +0000 (12:38 +0000)]
Syntax highlighting for focus/unfocus
Claudio Sacerdoti Coen [Fri, 26 May 2006 11:18:47 +0000 (11:18 +0000)]
Great optimization for eat_prods: if the type of the head of the application is meta_closed,
Andrea Asperti [Fri, 26 May 2006 11:08:29 +0000 (11:08 +0000)]
1) variables occurring only in proofs anre not relocated
Claudio Sacerdoti Coen [Fri, 26 May 2006 10:10:39 +0000 (10:10 +0000)]
Profiling code removed.
Andrea Asperti [Fri, 26 May 2006 08:03:20 +0000 (08:03 +0000)]
Bug fixed: the syntax "?n" used to be broken. It tried a string_of_int "?n".
Claudio Sacerdoti Coen [Thu, 25 May 2006 17:37:27 +0000 (17:37 +0000)]
More documentation.
Claudio Sacerdoti Coen [Thu, 25 May 2006 17:13:58 +0000 (17:13 +0000)]
More documentation.
projects / helm.git / log