used the new metadataConstraint function to retrieve equalities from the library

fixed equalities_for_goal

the old compute_eq_weight is back (no more max)

fixed generation of letins

added a metas_of_term implemented using sets instead of lists (avoids some stack overflows)

file names patched

patched

more work for the generic auto parameters

added the geniric
  auto params
syntax and the auto superposition tactic

forgotten commit

RELATIONAL-ARITHMETICS updated

- fwd concrete syntax fixed
- decompose, fwd, lapply documentation fixed

garbage collection of dead equalities implemented

- added some documentation on the fwd tatcic
- lapply concrete imput syntax fixed

Patterns are now documented.
But: how do we do multiple selections in matita?

axioms removed

hack to allow (**)

typo cpying the formal semantic

reorganized guiven_clause to work with the on_the_fly simplification of goals during ghr infer_goals step

demodulation of goal activated again.
to deactivate it, the check_if_goal_set_us_solved should be moved after the infeer_goal step

some experiments

added (but still unused) remove_local_context

added (but not yet used) remove_local_context
weight of non oriented equations decreased

Utils.compare_terms instead of compare_weights
fold_right -> fold_right

occur_check and unification fixed. now Meta(i,[]) and Meta(i,[...]) are
considered the same.

...

- some fixes regarding URIs of equality that now should be coherent with the
  one of the goal
- eliminated the stack overflow issue when building the proof

instead of including library_notation we include logic/equality that is smaller

fix

contribution on relational arithmetics started

fixed

fixes

ecco le gatte da pelare

ancient bug solved. if the term is (eq TY A B) the signature of A and B was
ignored if TY was a Sort.

some more on equalities

added log.120.orsay.txt and comparison

some examples of the new ApplyS tactic

examples of applyS

Apply-Silvie tactic added!

added applyS

some fixed done in Orsay:
- supL is called on both sides if the equation is not oriented
- contextualize_rewrites fixed if multiple equalities are used (equalities on different types)

exported 2 functions needed by applyS

...

default constants are now the matita standard library ones and not the one from Coq.
the makefile should work on every checkout, since the path for the TPTP stuff is not hardcoded, but ppoint to the TPTP-VERSION/ directory in the user's home.

bumped date

better wording of a sentence

center figures in HTML version of the manual using CSS

changed install target so that figures are instaled as well

fixed bad spellend "stantard"

removed old ignore lines about matita.conf.xml.ROLE

Enrico: bugfix, remove depend.errors upon destroy

removed old debugging print

relocation of developments.png

adding the developments screenshot

cosmetic: better placement of news box

- added news section
- added <a name ...> on each level 2 heading

added mention of the two mailing lists we have

download.shtml is now valid xhtml 1.0 strict

bumped date

new path for XSLT sytlesheets

typo: titleabbrev stuff should not be bold

added generation of quick reference card of tactic syntax

- distributed matitaGeneratedGui.ml (needed)
- when distributed 'world' is the default target

generate gui code upon distribution

distribute more stuff
added an install target to the manual makefile

reordered author list

use the install target of the manual

updated some distributed stuff

recursive invocation of distr_pre

filled README, BUGS, and other files useful for the distribution

moved benchmnarks/ dir outside of components/

aligned matita logo to the left

added shortcut targets

added dummy <entry /> to make yelp happy

- better formatting/factorization of tables used for grammar description
- improved rendering toward TeX

fix in the development page

- slight fix in lapply syntax
- Ferruccio Guidi is NOT a former member :)

added support for displaying the list of papers related to matita in the documentation page (currently commented out)

added reference to the online version of the manual

added deps, create target dir if missing

ignore generated stuff

tiny version of the logo

keeping the generated manual on svn is overkilling

generate deps on the fly
added dep on the stylesheets

removed overkilling info for our manual

consistent naming of the calculus

css stylesheets for the on-line manual

factorized legal stuff like other chapters

manual regenerated

new documentation for the decompose tactic

first generation of manual from docbook
better Makefile

added automatic generation of the manual

yet another screenshot

added screenshots describing matita features

- all final shtml are now well formed XML documents
- added a link to the logo in the top left corner
- structured and commented the CSS stylesheet
- added $Id$ where missing
- the Makefile no longer builds images when invoked with no targets

wording

- added a real-life index page
- removed the label 'matita' on the top-left logo
- added a big 'matita' label for the index page
- factorized common stuff that goes inside <head> in a new SSI

rewored website layout and internal structure:
- moved menu bar to the left
- added logo on the top left
- added headings

scaled down

scaled down