]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agofixed
Enrico Tassi [Fri, 16 Jun 2006 19:07:08 +0000 (19:07 +0000)]
fixed

18 years agofixes
Enrico Tassi [Fri, 16 Jun 2006 18:51:18 +0000 (18:51 +0000)]
fixes

18 years agoecco le gatte da pelare
Enrico Tassi [Fri, 16 Jun 2006 16:06:41 +0000 (16:06 +0000)]
ecco le gatte da pelare

18 years agoancient bug solved. if the term is (eq TY A B) the signature of A and B was
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.

18 years agosome more on equalities
Enrico Tassi [Fri, 16 Jun 2006 11:47:25 +0000 (11:47 +0000)]
some more on equalities

18 years agoadded log.120.orsay.txt and comparison
Enrico Tassi [Fri, 16 Jun 2006 09:03:24 +0000 (09:03 +0000)]
added log.120.orsay.txt and comparison

18 years agosome examples of the new ApplyS tactic
Andrea Asperti [Thu, 15 Jun 2006 09:39:55 +0000 (09:39 +0000)]
some examples of the new ApplyS tactic

18 years agoexamples of applyS
Andrea Asperti [Thu, 15 Jun 2006 09:39:20 +0000 (09:39 +0000)]
examples of applyS

18 years agoApply-Silvie tactic added!
Andrea Asperti [Thu, 15 Jun 2006 09:38:42 +0000 (09:38 +0000)]
Apply-Silvie tactic added!

18 years agoadded applyS
Andrea Asperti [Thu, 15 Jun 2006 09:38:08 +0000 (09:38 +0000)]
added applyS

18 years agosome fixed done in Orsay:
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)

18 years agoexported 2 functions needed by applyS
Andrea Asperti [Thu, 15 Jun 2006 09:35:47 +0000 (09:35 +0000)]
exported 2 functions needed by applyS

18 years ago...
Andrea Asperti [Thu, 15 Jun 2006 09:24:46 +0000 (09:24 +0000)]
...

18 years agodefault constants are now the matita standard library ones and not the one from Coq.
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.

18 years agobumped date
Stefano Zacchiroli [Wed, 14 Jun 2006 15:04:13 +0000 (15:04 +0000)]
bumped date

18 years agocenter figures in HTML version of the manual using CSS
Stefano Zacchiroli [Wed, 14 Jun 2006 14:41:44 +0000 (14:41 +0000)]
center figures in HTML version of the manual using CSS

18 years agochanged install target so that figures are instaled as well
Stefano Zacchiroli [Wed, 14 Jun 2006 14:40:06 +0000 (14:40 +0000)]
changed install target so that figures are instaled as well

18 years agofixed bad spellend "stantard"
Stefano Zacchiroli [Wed, 14 Jun 2006 14:33:57 +0000 (14:33 +0000)]
fixed bad spellend "stantard"

18 years agoremoved old ignore lines about matita.conf.xml.ROLE
Stefano Zacchiroli [Wed, 14 Jun 2006 14:33:23 +0000 (14:33 +0000)]
removed old ignore lines about matita.conf.xml.ROLE

18 years agoEnrico: bugfix, remove depend.errors upon destroy
Stefano Zacchiroli [Wed, 14 Jun 2006 14:32:46 +0000 (14:32 +0000)]
Enrico: bugfix, remove depend.errors upon destroy

18 years agoremoved old debugging print
Stefano Zacchiroli [Wed, 14 Jun 2006 14:30:32 +0000 (14:30 +0000)]
removed old debugging print

18 years agorelocation of developments.png
Enrico Tassi [Wed, 14 Jun 2006 14:14:11 +0000 (14:14 +0000)]
relocation of developments.png

18 years agoadding the developments screenshot
Enrico Tassi [Wed, 14 Jun 2006 14:08:28 +0000 (14:08 +0000)]
adding the developments screenshot

18 years agobumped date
Stefano Zacchiroli [Tue, 13 Jun 2006 14:24:25 +0000 (14:24 +0000)]
bumped date

18 years agotypo: titleabbrev stuff should not be bold
Stefano Zacchiroli [Tue, 13 Jun 2006 14:22:43 +0000 (14:22 +0000)]
typo: titleabbrev stuff should not be bold

18 years agoadded generation of quick reference card of tactic syntax
Stefano Zacchiroli [Tue, 13 Jun 2006 14:18:33 +0000 (14:18 +0000)]
added generation of quick reference card of tactic syntax

18 years ago- distributed matitaGeneratedGui.ml (needed)
Stefano Zacchiroli [Tue, 13 Jun 2006 12:03:51 +0000 (12:03 +0000)]
- distributed matitaGeneratedGui.ml (needed)
- when distributed 'world' is the default target

18 years agogenerate gui code upon distribution
Stefano Zacchiroli [Tue, 13 Jun 2006 11:42:28 +0000 (11:42 +0000)]
generate gui code upon distribution

18 years agodistribute more stuff
Stefano Zacchiroli [Tue, 13 Jun 2006 10:21:57 +0000 (10:21 +0000)]
distribute more stuff
added an install target to the manual makefile

18 years agoreordered author list
Stefano Zacchiroli [Tue, 13 Jun 2006 10:21:28 +0000 (10:21 +0000)]
reordered author list

18 years agoupdated some distributed stuff
Stefano Zacchiroli [Tue, 13 Jun 2006 10:00:50 +0000 (10:00 +0000)]
updated some distributed stuff

18 years agorecursive invocation of distr_pre
Stefano Zacchiroli [Tue, 13 Jun 2006 09:54:21 +0000 (09:54 +0000)]
recursive invocation of distr_pre

18 years agofilled README, BUGS, and other files useful for the distribution
Stefano Zacchiroli [Tue, 13 Jun 2006 09:53:27 +0000 (09:53 +0000)]
filled README, BUGS, and other files useful for the distribution

18 years agomoved benchmnarks/ dir outside of components/
Stefano Zacchiroli [Tue, 13 Jun 2006 08:33:55 +0000 (08:33 +0000)]
moved benchmnarks/ dir outside of components/

18 years agoadded shortcut targets
Stefano Zacchiroli [Mon, 12 Jun 2006 11:36:36 +0000 (11:36 +0000)]
added shortcut targets

18 years agoadded dummy <entry /> to make yelp happy
Stefano Zacchiroli [Mon, 12 Jun 2006 11:27:15 +0000 (11:27 +0000)]
added dummy <entry /> to make yelp happy

18 years ago- better formatting/factorization of tables used for grammar description
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

18 years ago- slight fix in lapply syntax
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 :)

18 years agogenerate deps on the fly
Stefano Zacchiroli [Sat, 10 Jun 2006 16:24:25 +0000 (16:24 +0000)]
generate deps on the fly
added dep on the stylesheets

18 years agoremoved overkilling info for our manual
Stefano Zacchiroli [Sat, 10 Jun 2006 16:24:03 +0000 (16:24 +0000)]
removed overkilling info for our manual

18 years agoconsistent naming of the calculus
Stefano Zacchiroli [Sat, 10 Jun 2006 16:21:25 +0000 (16:21 +0000)]
consistent naming of the calculus

18 years agocss stylesheets for the on-line manual
Stefano Zacchiroli [Sat, 10 Jun 2006 16:20:58 +0000 (16:20 +0000)]
css stylesheets for the on-line manual

18 years agofactorized legal stuff like other chapters
Stefano Zacchiroli [Sat, 10 Jun 2006 16:20:44 +0000 (16:20 +0000)]
factorized legal stuff like other chapters

18 years agonew documentation for the decompose tactic
Ferruccio Guidi [Sat, 10 Jun 2006 14:44:43 +0000 (14:44 +0000)]
new documentation for the decompose tactic

18 years agoMore documentation committed.
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 15:54:19 +0000 (15:54 +0000)]
More documentation committed.

18 years agoSyntactic bug changed: t in "unfold t" must be a tactic_term, not a term
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

18 years agoTactics are now documented using bolds for terminal symbols.
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 15:00:58 +0000 (15:00 +0000)]
Tactics are now documented using bolds for terminal symbols.

18 years ago1. the default for the default equality/absurd/true/false URIs used to be
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

18 years ago[a-z] syntax documented
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 14:37:20 +0000 (14:37 +0000)]
[a-z] syntax documented

18 years agoLexical conventions documented.
Claudio Sacerdoti Coen [Fri, 9 Jun 2006 14:33:16 +0000 (14:33 +0000)]
Lexical conventions documented.

18 years agoNotation for congruent.
Andrea Asperti [Fri, 9 Jun 2006 13:14:11 +0000 (13:14 +0000)]
Notation for congruent.
Restyling of fermat's little theorem with tynicals.

18 years agothe Matita manual is now convertible to a decent .tex that is processable both
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

18 years agodevelopments added
Enrico Tassi [Thu, 8 Jun 2006 12:00:35 +0000 (12:00 +0000)]
developments added

18 years agoadded "dumb" test target
Stefano Zacchiroli [Wed, 7 Jun 2006 16:38:34 +0000 (16:38 +0000)]
added "dumb" test target

18 years agoAttempt to make our markup respect the docbook specification(!), major changes
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.

18 years agobug fixed in doc
Stefano Zacchiroli [Mon, 5 Jun 2006 11:38:24 +0000 (11:38 +0000)]
bug fixed in doc

18 years ago(co)inductive type declarations are now documented
Claudio Sacerdoti Coen [Mon, 5 Jun 2006 11:27:13 +0000 (11:27 +0000)]
(co)inductive type declarations are now documented

18 years agoRecord syntax is now described.
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.

18 years agoimplemented tinycals:
Stefano Zacchiroli [Thu, 1 Jun 2006 15:32:34 +0000 (15:32 +0000)]
implemented tinycals:
- 1,2,3: ...
- *:

18 years agocommented the finally function
Stefano Zacchiroli [Thu, 1 Jun 2006 15:27:50 +0000 (15:27 +0000)]
commented the finally function

18 years agofix
Enrico Tassi [Thu, 1 Jun 2006 13:28:19 +0000 (13:28 +0000)]
fix

18 years ago...
Enrico Tassi [Thu, 1 Jun 2006 11:36:50 +0000 (11:36 +0000)]
...

18 years ago...
Enrico Tassi [Thu, 1 Jun 2006 11:23:51 +0000 (11:23 +0000)]
...

18 years agouse the appropriate chain of transormations for pretty printing term
Stefano Zacchiroli [Thu, 1 Jun 2006 10:52:11 +0000 (10:52 +0000)]
use the appropriate chain of transormations for pretty printing term

18 years agomade pp_term parametric and explained the proper way of solving the object pretty...
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

18 years agoBug fixed that made theory rendering bugged after visiting a whelp search page.
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.

18 years agobugfix: rely on byte count instead of mixing byte and character count
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

18 years agoSubsumption_subst must be applied to the initial proof before passing
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.

18 years agoSigma algebras and measurable maps defined.
Claudio Sacerdoti Coen [Wed, 31 May 2006 17:12:12 +0000 (17:12 +0000)]
Sigma algebras and measurable maps defined.

18 years agoCommitted a first experiment in the formalization of Lebesgue dominated
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.

18 years ago\n restored
Enrico Tassi [Wed, 31 May 2006 13:54:57 +0000 (13:54 +0000)]
\n restored

18 years agofixed proofs, contextualization should now work.
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.

18 years ago1. the default encoding for the stylesheets is now UTF8
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

18 years agomatita.txt updated
Claudio Sacerdoti Coen [Tue, 30 May 2006 14:56:58 +0000 (14:56 +0000)]
matita.txt updated

18 years agoBug fixed: theories were handled as base uris, not as uris of files.
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.

18 years agoletin are now sorted properly.
Enrico Tassi [Tue, 30 May 2006 11:50:51 +0000 (11:50 +0000)]
letin are now sorted properly.

18 years agofixed proof generation again
Enrico Tassi [Tue, 30 May 2006 10:44:55 +0000 (10:44 +0000)]
fixed proof generation again

18 years agouse the proper top level function to parse terms
Claudio Sacerdoti Coen [Tue, 30 May 2006 10:33:42 +0000 (10:33 +0000)]
use the proper top level function to parse terms

18 years agoZACK: export a top level function for parsing terms, it can't be bypassed due to...
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

18 years ago...
Enrico Tassi [Tue, 30 May 2006 09:26:15 +0000 (09:26 +0000)]
...

18 years agoA -> Univ
Enrico Tassi [Tue, 30 May 2006 09:19:14 +0000 (09:19 +0000)]
A -> Univ

18 years agocanonical and contextualize_rewrites are back, they seem to work now...
Enrico Tassi [Tue, 30 May 2006 09:09:37 +0000 (09:09 +0000)]
canonical and contextualize_rewrites are back, they seem to work now...

18 years agothe function to create on the fly a symmetry step has been moved to equality
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

18 years agoadded our poor results to CASC 2005
Enrico Tassi [Tue, 30 May 2006 08:42:24 +0000 (08:42 +0000)]
added our poor results to CASC 2005

18 years agoZACK: ported to the latest ocaml-http API
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:14:33 +0000 (08:14 +0000)]
ZACK: ported to the latest ocaml-http API

18 years agoZACK: 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

18 years agoported 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

18 years agoZACK: 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

18 years agoported 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

18 years agobugfix: when creating a daemon spec _use_ the auto_close value passed as argument...
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

18 years ago- removed Http_daemon.{start,start\}
Stefano Zacchiroli [Mon, 29 May 2006 20:52:22 +0000 (20:52 +0000)]
- removed Http_daemon.{start,start\}

18 years agoadded some logs
Enrico Tassi [Mon, 29 May 2006 20:44:57 +0000 (20:44 +0000)]
added some logs

18 years agofix
Enrico Tassi [Mon, 29 May 2006 20:41:16 +0000 (20:41 +0000)]
fix

18 years agocommitted the base utils for TPTP processing
Enrico Tassi [Mon, 29 May 2006 20:40:35 +0000 (20:40 +0000)]
committed the base utils for TPTP processing

18 years agoadded finally function
Stefano Zacchiroli [Mon, 29 May 2006 20:33:30 +0000 (20:33 +0000)]
added finally function

18 years agoprofilings are printed
Enrico Tassi [Mon, 29 May 2006 20:32:58 +0000 (20:32 +0000)]
profilings are printed

18 years ago- proofs by subsumption now add a symmetry step if needed
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

18 years agoforces bash as Makefile SHELL
Stefano Zacchiroli [Mon, 29 May 2006 20:27:57 +0000 (20:27 +0000)]
forces bash as Makefile SHELL

18 years agoensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:36:36 +0000 (17:36 +0000)]
ensure connections get closed after having been served

18 years agolowered debugging level
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:34:16 +0000 (17:34 +0000)]
lowered debugging level