factorized legal stuff like other chapters

new documentation for the decompose tactic

More documentation committed.

Syntactic bug changed: t in "unfold t" must be a tactic_term, not a term

Tactics are now documented using bolds for terminal symbols.

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

[a-z] syntax documented

Lexical conventions documented.

Notation for congruent.
Restyling of fermat's little theorem with tynicals.

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

developments added

added "dumb" test target

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.

bug fixed in doc

(co)inductive type declarations are now documented

Record syntax is now described.
More &TODO; put here and there.

implemented tinycals:
- 1,2,3: ...
- *:

commented the finally function

fix

...

...

use the appropriate chain of transormations for pretty printing term

made pp_term parametric and explained the proper way of solving the object pretty printing problem

Bug fixed that made theory rendering bugged after visiting a whelp search page.

bugfix: rely on byte count instead of mixing byte and character count

Subsumption_subst must be applied to the initial proof before passing
it to build_proof_goal.

Sigma algebras and measurable maps defined.

Committed a first experiment in the formalization of Lebesgue dominated
convergence theorem: basic set theory and classical topology definitions.

\n restored

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.

1. the default encoding for the stylesheets is now UTF8
2. committed a few changes in search.xsl that had never been committed before

matita.txt updated

Bug fixed: theories were handled as base uris, not as uris of files.

letin are now sorted properly.

fixed proof generation again

use the proper top level function to parse terms

ZACK: export a top level function for parsing terms, it can't be bypassed due to the Obj.magic trick

...

A -> Univ

canonical and contextualize_rewrites are back, they seem to work now...

the function to create on the fly a symmetry step has been moved to equality

added our poor results to CASC 2005

ZACK: ported to the latest ocaml-http API

ZACK: ported to the latest ocaml-http API

ported to the latest ocaml-http API

ZACK: ported to the latest ocaml-http API

ported to the latest ocaml-http API

bugfix: when creating a daemon spec _use_ the auto_close value passed as argument instead of ignoring it

- removed Http_daemon.{start,start\}

added some logs

fix

committed the base utils for TPTP processing

added finally function

profilings are printed

- 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

forces bash as Makefile SHELL

ensure connections get closed after having been served

lowered debugging level

ensure connections get closed after having been served

OCAMLPATH is not overrid if already defined

ensure connections get closed after having been served

ensure connections get closed after having been served

bugfix:
- properties where applied and then discarded
- useless assert false removed

ensure connections get closed after having been served

ensure connections get closed after having been served

bug fix: use an (un)marshaller for get_opt instead of a getter

OCAMLPATH is no longer overrid if already set in current environment

Bug fixed in fresh_name_generator: the function used to fail on beta redexes. Fixed trivially without
introducing yet another whd.

added (TODO) section on tacticals)

weak equality on meta used when replacing.
updated to the new goal_proof

added the rule field to goal_proof.
fixed the SupL proof generation (but I think the fix should not be here)

- fixed a bug in unification (not sure in the right way)

CALS tables enriched to make (crappy) docbook stylesheets happy.

Documentation fixed.

New documentation.

More documentation.

More documentation.

Recently introduced bug in CicRefine.eat_prods fixed: a whd was now missing.
Added a test to verify the performances of refinement.

Syntax highlighting for focus/unfocus

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.

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)

Profiling code removed.

Bug fixed: the syntax "?n" used to be broken. It tried a string_of_int "?n".

More documentation.

More documentation.

More doc

added a file useful to load all notation
(use include' and not include).

Added debug menu item to restrict disambiguation to the first pass only.

Axioms are not allowed with the syntax: "axiom name: type.".

svn:ignore fixed (again)

svn:ignore fixed

matita.txt updated

added important comment

fixed LetIn proofs

added again stuff for profiling

added dependency on Str

...

added stuff for profiling macros

- code cleanup, especialli in Indexing where all the goal related functions have
  been revised
- proofs are now factorized with LetIn
- support for profiling

generation of existential variables fixed