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)

1. Macros are now handled using an execption that is caught by matitacLib
   (raising an error) or matitaScript. As a result matitaScript is now simpler.
2. svn:ignore property refined for several directories in ocaml

ported to ocaml 3.09.1

ported to ocaml 3.09.1

bugfix, removed an hard coded instances of ocaml ABI version

ported to ocaml 3.09.1

ported to ocaml 3.09.1

fix

beauty\!

beauty\!

fix

fix

fix

fix

more fix

fix

attempt to move nightly profiling to svn

removed spurious CVSROOT from the old repository

test commit

removed prova

prova

updated

minor fixes (-nodb works again)

Added parameter first_statement_only to the functions in matitaEngine

alias diffing/insertion is now handled by matitaEngine (invoked both
by matita and matitac)

Makefiles made less verbose.

fix

fix

fix

fix

fix

fix

fix

...

fixed -f in clean
make tests now compiles coq.ma

fix

fix

reimplemented specific marshallars on top of generic HMarshal marshaller

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

added generic marshaller

fix