]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

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

18 years agoOCAMLPATH is not overrid if already defined
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:20:16 +0000 (17:20 +0000)]
OCAMLPATH is not overrid if already defined

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

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

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

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

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

18 years agobug fix: use an (un)marshaller for get_opt instead of a getter
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

18 years agoOCAMLPATH is no longer overrid if already set in current environment
Stefano Zacchiroli [Mon, 29 May 2006 13:49:53 +0000 (13:49 +0000)]
OCAMLPATH is no longer overrid if already set in current environment

18 years agoBug fixed in fresh_name_generator: the function used to fail on beta redexes. Fixed...
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.

18 years agoadded (TODO) section on tacticals)
Stefano Zacchiroli [Mon, 29 May 2006 11:56:28 +0000 (11:56 +0000)]
added (TODO) section on tacticals)

18 years agoweak equality on meta used when replacing.
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

18 years agoadded the rule field to 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)

18 years ago- fixed a bug in unification (not sure in the right way)
Enrico Tassi [Sun, 28 May 2006 16:07:33 +0000 (16:07 +0000)]
- fixed a bug in unification (not sure in the right way)

18 years agoCALS tables enriched to make (crappy) docbook stylesheets happy.
Claudio Sacerdoti Coen [Fri, 26 May 2006 15:58:47 +0000 (15:58 +0000)]
CALS tables enriched to make (crappy) docbook stylesheets happy.

18 years agoDocumentation fixed.
Claudio Sacerdoti Coen [Fri, 26 May 2006 15:39:29 +0000 (15:39 +0000)]
Documentation fixed.

18 years agoNew documentation.
Claudio Sacerdoti Coen [Fri, 26 May 2006 15:14:41 +0000 (15:14 +0000)]
New documentation.

18 years agoMore documentation.
Claudio Sacerdoti Coen [Fri, 26 May 2006 14:18:09 +0000 (14:18 +0000)]
More documentation.

18 years agoMore documentation.
Claudio Sacerdoti Coen [Fri, 26 May 2006 13:41:55 +0000 (13:41 +0000)]
More documentation.

18 years agoRecently introduced bug in CicRefine.eat_prods fixed: a whd was now missing.
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.

18 years agoSyntax highlighting for focus/unfocus
Claudio Sacerdoti Coen [Fri, 26 May 2006 12:38:42 +0000 (12:38 +0000)]
Syntax highlighting for focus/unfocus

18 years agoGreat optimization for eat_prods: if the type of the head of the application is meta_...
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.

18 years ago1) variables occurring only in proofs anre not relocated
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)

18 years agoProfiling code removed.
Claudio Sacerdoti Coen [Fri, 26 May 2006 10:10:39 +0000 (10:10 +0000)]
Profiling code removed.

18 years agoBug fixed: the syntax "?n" used to be broken. It tried a string_of_int "?n".
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".

18 years agoMore documentation.
Claudio Sacerdoti Coen [Thu, 25 May 2006 17:37:27 +0000 (17:37 +0000)]
More documentation.

18 years agoMore documentation.
Claudio Sacerdoti Coen [Thu, 25 May 2006 17:13:58 +0000 (17:13 +0000)]
More documentation.

18 years agoMore doc
Claudio Sacerdoti Coen [Thu, 25 May 2006 14:33:13 +0000 (14:33 +0000)]
More doc

18 years agoadded a file useful to load all notation
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).

18 years agoAdded debug menu item to restrict disambiguation to the first pass only.
Claudio Sacerdoti Coen [Thu, 25 May 2006 12:05:58 +0000 (12:05 +0000)]
Added debug menu item to restrict disambiguation to the first pass only.

18 years agoAxioms are not allowed with the syntax: "axiom name: type.".
Claudio Sacerdoti Coen [Thu, 25 May 2006 10:24:34 +0000 (10:24 +0000)]
Axioms are not allowed with the syntax: "axiom name: type.".

18 years agosvn:ignore fixed (again)
Claudio Sacerdoti Coen [Thu, 25 May 2006 10:05:22 +0000 (10:05 +0000)]
svn:ignore fixed (again)

18 years agosvn:ignore fixed
Claudio Sacerdoti Coen [Thu, 25 May 2006 10:04:39 +0000 (10:04 +0000)]
svn:ignore fixed

18 years agomatita.txt updated
Claudio Sacerdoti Coen [Thu, 25 May 2006 08:56:12 +0000 (08:56 +0000)]
matita.txt updated

18 years agoadded important comment
Andrea Asperti [Tue, 23 May 2006 12:07:36 +0000 (12:07 +0000)]
added important comment

18 years agofixed LetIn proofs
Andrea Asperti [Tue, 23 May 2006 11:56:39 +0000 (11:56 +0000)]
fixed LetIn proofs

18 years agoadded again stuff for profiling
Enrico Tassi [Tue, 23 May 2006 08:07:25 +0000 (08:07 +0000)]
added again stuff for profiling

18 years agoadded dependency on Str
Enrico Tassi [Tue, 23 May 2006 08:06:07 +0000 (08:06 +0000)]
added dependency on Str

18 years ago...
Enrico Tassi [Tue, 23 May 2006 08:05:09 +0000 (08:05 +0000)]
...

18 years agoadded stuff for profiling macros
Andrea Asperti [Tue, 23 May 2006 08:03:18 +0000 (08:03 +0000)]
added stuff for profiling macros

18 years ago- code cleanup, especialli in Indexing where all the goal related functions have
Enrico Tassi [Mon, 22 May 2006 15:06:42 +0000 (15:06 +0000)]
- code cleanup, especialli in Indexing where all the goal related functions have
  been revised
- proofs are now factorized with LetIn
- support for profiling

18 years agogeneration of existential variables fixed
Enrico Tassi [Sat, 20 May 2006 12:23:02 +0000 (12:23 +0000)]
generation of existential variables fixed