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

more static libs for matitaprover

see BOO025-1 as an example of failure if (mot p) is commented out.

added

matitaprover

eta_fix default to false

Revert of the previous situation: when an identifier has no universe all the
passes that does not use the library are doomed to fail and the user will
be asked how to instantiate everyn identifier (not withstanding performances).
Now if an identifier has no universe we look for its interpretations in the
library.

trans chains even inside letins body

avoid collapsing node that does not need to be, i.e.:
- nodes with no outgoing edges
- nodes which have not been expanded before

removed abstractios for dummy metavariables when generating letins body

reorganization

bugfix: proper computation of the amount of new node shown upon expand

added -dot to generate dot files

- added to the cicBrowser support for displaying recursive direct/inverse
  dependencies of a given object. To integrate this with cicBrowser's history
  also added a new URI scheme: metadata:/deps/(forward|backward)/URI, where URI
  is the object URI without the trailing "cic:"
- removed automatic stripping of #xpointer(...) from URIs of inductive types

New module to extract from the Db direct and inverse dependencies starting from
a given URI. Both single step and recursive (in graph form) dependencies are
supported.

exported position_prefix (so that it can be looked up from elsewhere)

use double quotes around escaped URIs, single quotes fail when the URI contains
a '\'' character

- enable header to output graphs attributes and graph-wide node and edge
  attributes
- quote nodes only when needed

- pipe graphviz markup to tred before generating png/map output to get rid of
  transitive dependencies
- added method center_on_href to clamp viewport so that a given node is visible
  (actually it is not a real "center"ing ...)

Bug fixed in rewrite in multiple hypothesis and/or conclusion: a lifting was
missing, as usual :-)