]>
matita.cs.unibo.it Git - helm.git/log
Stefano Zacchiroli [Tue, 13 Jun 2006 10:21:28 +0000 (10:21 +0000)]
reordered author list
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 [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:13:05 +0000 (08:13 +0000)]
- slight fix in lapply syntax
- Ferruccio Guidi is NOT a former member :)
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
Ferruccio Guidi [Sat, 10 Jun 2006 14:44:43 +0000 (14:44 +0000)]
new documentation for the decompose tactic
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
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 15:00:58 +0000 (15:00 +0000)]
Tactics are now documented using bolds for terminal symbols.
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.
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.
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
it to build_proof_goal.
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
convergence theorem: basic set theory and classical topology definitions.
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.
the empty context is not a term with an open (Rel 1), but a
a term with a (Cic.Implicit(Some `Hole)) so that it can't bw confused with a
Rel to the last Hypothesis.
Claudio Sacerdoti Coen [Tue, 30 May 2006 16:50:33 +0000 (16:50 +0000)]
1. the default encoding for the stylesheets is now UTF8
2. committed a few changes in search.xsl that had never been committed before
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
- a little optimization for Equality.depend (just to aviod te exponenetial
factor, but should be made faster)
- restored names in Lambda abstraction that give infos about the step they
represent
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:
- properties where applied and then discarded
- useless assert false removed
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
introducing yet another whd.
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.
updated to the new goal_proof
Enrico Tassi [Sun, 28 May 2006 16:09:00 +0000 (16:09 +0000)]
added the rule field to goal_proof.
fixed the SupL proof generation (but I think the fix should not be here)
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.
Added a test to verify the performances of refinement.
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,
the construction of the spine of Prods and relative unification is skipped.
Andrea Asperti [Fri, 26 May 2006 11:08:29 +0000 (11:08 +0000)]
1) variables occurring only in proofs anre not relocated
2) during unification the resulting metasenv is cleaned of duplicates
(duplicates can only be variables in proofs, not in left/right)
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.
Claudio Sacerdoti Coen [Thu, 25 May 2006 14:33:13 +0000 (14:33 +0000)]
More doc
Enrico Tassi [Thu, 25 May 2006 14:10:17 +0000 (14:10 +0000)]
added a file useful to load all notation
(use include' and not include).