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 :-)

- added sql statements for querying forward and backward dependencies
- escaped uri which get embedded in sql statements

Submitted a test for inferencing of dependent types.

added sets of uri pairs (useful for edges between uris)
currently commented since not used ...

Ctr-C now cleans up (with a nice warning :-)

is_empty_listing fixed: the ls method normalizes away the .gz suffix

Serious bug fixed in simplify: sometimes terms wwere not closed because of
the use of the wrong replace function (that did not perform the required lifting).

baseuri for group.ma fixed

head_beta_reduce can now optionally perform delta reduction too

Unification improved to handle beta-delta conversion in most cases.
This is required to match Coq's unification for the porting of setoids.ma.

added split_nth

double quotes node identifiers

Baseuri of applys.ma fixed.

Quick&dirty patch to make Http_getter_storage.is_empty ignore {.moo,.metadata.lexicon} files.

dependeciesParsed fixed to parse URIs also in QSTRINGs
(because of alias id qstring = qstring)

legacy/coq.ma included

le_inv renamed to avoid conflicts with the automatically generated one.

rmdir_descend now works also on non existent dirs

magic number incremented (because of the new declarative commands)

libraryclean fixed to eradicate files generated from .ma files that do not
declare any object (e.g. legacy/coq.ma)

The dependencies parser is more robust w.r.t. to lexing errors.

...

evvai!

...

Added the computation of max_weight.

Added the computation of max_weight for equations in proofs.

added $Id$

use the graphviz pretty printer to generate graphviz markup for the coercions graph

moved graphviz pretty printer outside matita, so that it can be used by other components (e.g. from CoercDb to generated coercions graph)

use lablGraphviz to render the coercion graph and added a callback to follow hyperlinks there

generate dot files with attributes on nodes (instead of only edges), and added generation of the href attribute

added uri_of_carr

added pretty printer for dot files (it may need to be moved elsewhere in the future)

fixed the number of columns in the clusters table

Documentation date changed.

More commands documented.

bugfix: remove all generated temp files

added widget for rendering and interacting with graphs generated via graphviz

More commands documented.

More commands documented.

First skeleton of documentation for "other commands".

Missing copyright added to tactics/declarative.ml*

GrafiteAst.Quit (unused) removed.

GrafiteAst.Print (unused) removed.

GrafiteAst.Search_pat and GrafiteAst.Search_term (both unused) removed.

restored the 2 ways of pasting: both "as term" and "as pattern" are available again

paramodulation is not a stand alone tactic: doc fixed.

More documentation.

dependences updated again :)

updated dependences

First experimental version of the declarative proof language for Matita.
Supported commands so far:
  assume id: term
  suppose term (id)
  by term done
  by term we proved term (id)
  we need to prove term (id)

More TODO items in the documentation.

- removed Positive and Negative (all is positive)
- eq_f and eq_f1 used in proofs

fixed

...

- cheanges for the new coercion stuff (including the generated graph)
- new test for coercions
- new test for tinycals

renamed the coercion

improved coercions support:
- multiple coercions from the same carrier are allowed
- coercions are hidden from the proof too
- a new function to print proof in text mode added

fixed 1,2: and *: according to the camera ready semantics

added flatten_map