contentPp.ml (dead code) removed

Dead code (that produces an ugly rendering) removed.

removing unnecessary files

- some theorems from levels_defs
- a new problem

ok up to tau0

Missing alias added.

Preamble is now working properly and it does not include unwanted aliases.

error in preamble.ma

subst0 completed

some theorems about getl

Bugs fixed:
 1. matitamake now correctly creates dependencies of the form "A/f.mo: ..." (it used to create
    useless dependencies of the form "/T/A/f.mo: ...")
 2. matitamake is now more (indeed too much) verbose when matitadep fails

matitadep used to raise Not_found on empty files and in some other occasions.
Fixed.

removing unnecessary file

dependences fixed

plist added

removing working file

new theorems

fixed coercions. composite can't occur if to funclass

fixed includes

other working theorems + iso_trans axiomatized (proof saved in problems)

BIG FAT COMMIT REGARDING COERCIONS:
- multiple coercions from the same type
- coercions to funclass
- fixed cicPp for letin and pi
- improved coercions ma with a minimal test for funclass
- cheanged XML and Ast to support `Coercion ARITY label
- added syntax:
  coercion URI ARITY
  recordfield :ARITY> type
- added topological sorting module (funcotr) in extlib
- abstracted graphviz to allow non strict and tred graphs
- tentative (not yet properly done) of hiding coercions in content
- fixed a problem in metadata contraints iof there are no constraints
- renamed/moved/commented some functions (eat_prod related) in the refiner
- crossed fingers

firs error: iso/props

More aliases.

no-indent

removed non XML comment line

the in clause of the match costruction was wrongly output

Aliases are now wrote down even during the first pass.
The only case they are not written down is that of multiple passes.
This makes the scripts more robusts and faster.
We still need (more and more) one shot aliases.

matitac now fails if it tries to insert a new alias

new organization of the Base and LambdaDelta modules

Generation of inductive and inversion principles for mutual
inductive types (before only single types were allowed).

Bug fixing. If the inductive types do not occur in t, t is
strictly positive.

moving files

rebuilt

LambdaDelta.ma and some slices of it that typecheck ok!

new problem:
generation of LambdaDelta.ma fails because of complex Cases costructions

Base.ma now ok!!

- semantics of tactic subst allmost fixed
- new tactical progress implemented (not working yet :( )

fixing the semantics of subst

a bit of improvement

aliases removed

added a preamble file with disambiguation information

- new tactic subst removes simple non recursive equalities from the context
- RELATIONAL updated to use the new tactic

cic/test.ml moved to binaries/utilities

Documentation for let-rec fixed.

test file with some bugs

- bumped year
- up to date FSF address

- Level-1: some problems solved
- legacy: one alias added

- Level-1: some fixes to the extraction procedure
- tactics: subst id now works (preliminary)

- makefile added

- record constructor alpha-converted

- Level-1: added two problems
- legacy: added some aliases
- CicNotationPp: fixed output syntax of records

- Level-1: added some problems
- legacy: some now aliases

- changed baseuri

- removed () around sorts

- added some aliases

changed baseuri

- added problem 2
- changed baseuri
- some fixes

- Unified    : some definitions of unified \lambda\delta
- level-1    : \lambda\delta exported from Coq (not working)
- RELATIONAL : added some notation
- cicNotation: some patches to the parser and pp to make them match

trying to make output notation parsable

some properties of NLE

- new legature == for \equiv used in the notation for NPlus
  FIXME: notation precedence not correct w.r.t. \to \land ...
- added notation for NLE
- added a comment to dependenciesParser.ml :p

new naming

removing old contrib dir

changing the contribution name

new naming

info about where to find LablGtkSourceView now

lablgtksourceview is moving to gna, removing the old stuff available here

...

...

new naming

new definitions

touched changelog, ready for a release!

new naming

bumped gmetadom dependencies to >= 0.2.4

- added a label_of_uri function to easily change node labels
- increased font size and use names as node labels (make CSC happy :))

More debugging output on stderr.

Automation enabled for declarative proofs. Cool.

"that is equivalent to" and "or equivalently" implemented in most situations.

All the declarative tactics now have a more or less bugged implementation.

Declarative tactics for rewriting steps, elimination of the existential
quantifier and elimination of conjunciton implemented.

Notation for the existential quantifier moved to core_notation.moo

New declarative commands (ast, pretty-printing and parsing only):
  [obtain term] = term by term
  by term we have term (id) and term (id)
  we proceed by induction on term to prove term
  the thesis becomes term
  by induciton hypothesis we know term
  case id [(id:term)]*

print_endline => prerr_endline

Patch to the unification to make the case (i l) vs (t l) work when i is
an inductive type and (t l) must be subject to weak head reduction.

Debug code commented out.

Elim now performs whd to find the inductive type.

added tinycals to the proof we frequently use for examples and screenshots

added test for reordering of goals when using the 1,2,3: tinycal

order is important

added definition of f_equal1. I think this file should not be inside the matita library!
once cercions from /\ to eq will be committed the definition should be replaced by two
coercion statement (that will generate the composite)

Bug fixed: a symbol alias Symb(s,0) now subsumes the case Symb(s,n) for each n.

Disambiguation passes simplified.

A compiling version of the library.

use the new graphviz pretty printer API

added missing dependency

equality now requires 2 extra parameters

removed reference to primes1.ma (now removed)

added timeout parameter to auto paramodulation.

more work on matitaprover (no more XML and buris are created).
now matita can start on a .p file.

more and more tests