Added header

looks fine to me

- moved section in place according to new organization
- commented the (missing) screenshot to enable compilation

new version

Matita header

font -1

Updated version

New reduction strategy (that behaves much better during simplification).
Unfortunately, the new reduction is a bit slower on one test (paramodulation).
To be investigated.

1. Back to nicer (and more comprehensible) notation (that cannot be used
   when more than one structure is in use at once).
2. The first definitions and theorems over groups.

"Hiding" notation for implicit coercion. Cool.

Some work...

A few experiments (with horrible results) using notation...

Aggiornato alla nuova gerarchia di moduli.

debug prints commented

some debug prints/stats

library ==> component

paramodulation is no longer a self-alone module

baseuri of coq.ma fixed

libraries.ps no longer in synch.

New dependencies!

Universes speedup:
1) the merging is done thinking that the working graph is probably bigger than
   a cleaned ugraph
2) a cache of already merged ugraph is added.

fast hack to fix decompilation with -nodb with the new getter.prefixes format

changed universes merging order: euristic which improve performances

Bug fixed (in Cast).

An embryonic kernel of the algebraic library.
Useful only to profile the universes :-)

subst_vars optimized for the explicit_named_subst=[] case (the most common
one)

Dead code removed and reindentation.

(Partial commit)
Improved version of cicReduction. Configurations can now be preserved as much
as possible (without need to go back to terms by means of unwind).
This allows the implementation of new strategies and removes a few sources of
inefficiences.

The commit is partial since not every strategy has been ported yet.

...

Bug fixed: the wrong context was used.

Dead code removed.

bugfix for missing parens: when the precedence does not change, parens are now added not only when there is a mismatch Left vs Right or vice versa but also when there is a mismatch Left vs Inner, Right vs Inner and vice versa.

Added recursive path ordering and demodulation tactic.

More informative error message.

fixed coercions undoooing

fixed

fix

fixed compilation order

fixes for paramodulation relocation
saturate(.opt) is now always compiled

fixed paramodulation trnsition

Removed calls to paramodulation.saturation.init

Moved paramodulation inside tactics.
Added a new (reduction) tactic demodulate.

ignore used to avoid Y warning

Dependency coq.moo.opt added to target tests.opt

Dead code removed.

Dead code removed.

mah...

fix

Added $SVNOPTION.

svn now uses $SVNOPTIONS;
this can be useful to set the release to be checked out in the crontab

New table bench_svn to keep the map "mark"==>"revision"

Hand-made generated inversion lemma.
It heavily uses the new tinycal features.

Code clean up.

cle introduced; ceq fixed

added $Id$

Dead code removed.

Dead code removed.

Dead code removed.

Dead code removed.

Warning Y fixed.

Dead code removed.

Dead code removed.

LIMIT 0,-1 no more valid --> removed

paramodulation now compiles with ocaml 3.09 in opt mode (added -for-pack)

The proofContext method now returns the empty context when no proof is ongoing.
This behaviour is compatible with the behaviour of proofMetasenv

Bug fixed in computation of the domain of records with left parameters.

changes location of coq.ma (now "legacy/coq.ma")

matita standard library is an include path per default

rebuilt

coq repository is legacy

added stdlib_dir entry

added buildTimeConf interface

moved coq.ma to library/legacy/

- new location for coq.ma
- better implementation of test related Makefile rules

do not generate deps for legacy URIs

avoid writing in read only baseuris

bumped year

added support for repository attributes

added sample entries with attributes

Old compare-terms function

removed debugging printing

added cleaning of .lexicon and .metadata files

ignoring the result of load_notation

Bux fixed: matita did not save the .lexicon files! (only matitac did)

$Id$ readded to paramodulation/utils.ml

Added a parameter (empty list) to load_notation.

added again the bin files

moved away broken files

New version of compare_weights.

fix

fix

moved to svn

Stupid bug of mine fixed: sometimes (Some ~-1) was used in place of None.
Moreover the userGoal was retrieved before setting it.

New version.

Bug fixed: the include_paths were no longer handled properly when matita was
launched outside a development. E.g.: ./matita library/nat/times.ma was no
longer working (./matita -I library library/nat/times.ma was)

Bug fixed: macros in the middle of a goto cursor or goto end-of-script were
not executed.

Explanation: the current goal was set only externally, but it is used by
macro disambiguation.

To fix the bug I have finally changed the type of a "lazy_macro" so that its
input is now a context. it used to be an integer, the selected goal; however,
the integer does not make sense since a macro can be invoked also when there is
no current proof.

Added $Id$ to every .ml file.

Added $Id$ to the file.

.cvsignore files removed (the svn:property property is used instead)