commit by user lroversi

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

Made a copy of basics/list.ma as a base for chapter 3.

commit by user andrea

commit by user enrico

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

Matitaweb: Fixed netplex.conf (which was changed by mistake in the previous commit).

Matitaweb: svn now skips empty commits.

commit by user andrea

Matitaweb: svn now skips empty add.

commit by user lroversi

Administrative commit restoring the repository to the usual shape.

commit by user ricciott

theory of ltpss completed!

commit by user andrea

commit by user andrea

commit by user andrea

update ...

update ...

- cpr_lsubs_conf proved! (was pr2_change)
- some "-" removed :)

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

refactoring completed!

Matitaweb: Fixed long-time bug with dependencies and makefiles.

Chapter 2

commit by user utente1

commit by user andrea

WARNING: major experimental change.

"include" is no longer turned into an "include alias"
when the file to be included is already loaded. This
greatly speeds up inclusion, at the price of having
to manually add some "include alias" here and there.

New version (by Wilmer). The main difference w.r.t. previous one
is that it should not normalize the hypotheses and the conclusion
without any need to do that.

BEWARE: this version seems to be a little buggy. See "Wilmer: XXX"
comments in CerCo files. I commit it anyway and let the debug to
Wilmer. It only fails in three places.

refactoring ...

refactoring ...

cpr_cast closed! (after a bugfix in the "destruct" tactic)

1. nInversion/nDestruct ported to work with jmeq properly
2. axiom streicherK in logic.ma replaced with a computational proof
3. library changed accordingly

Debugging code commented out.

Ported changes amde on the main branch:
1. Reintroduced a failure cache
2. Corrected a bug in subsumption
3. Crippled the search space of not-last (side) equational goals.

- Reintroduction of a failure chache
-r
-e, and those below, will be ignored--

    ng_tactics/nnAuto.ml

Matitaweb: fixed bugs in commit.

commit by user utente3

commit by user utente2

Matitaweb: added a titlebar to the GUI.

Matitaweb: more changes to commit (now almost usable).

commit by user utente

Matitaweb: several improvements to svn interface.
Some cosmetic changes.

news update

typos ...

- first version of xhtbl
- first version of ld_basic_2.html (generated)

- new stylesheets for xhtml pages (ld_web)
- typo corrected in ld_web.css

Matitaweb: test commit.

Matitaweb: commit test.

Matitaweb: commit test.

Matitaweb: commit test.

commit by user andrea

Matitaweb: implementation of file-flagging for keeping track of modified files
proceeds.

new version

commit by user andrea

commit by user andrea

Matitaweb file flag test.

commit by user andrea

commit by user andrea

- xhtbl.css is ready!
- images ar now in a dedicated directory

Matitaweb: test commit.

Matitaweb: test commit.

Matitaweb: test commit.

Matitaweb: test commit.

Matitaweb: Library test.

...

Matitaweb: Some bugfixes concerning file flags.

Matitaweb:
1) Added experimental update functionality
2) Flagged library files -synchronized, modified, conflicted, unmanaged-
   (partial implementation)
3) Various cosmetic changes

still new colors ...

bugfix in one of the new colors :)

bugfix in remote update

new colors for the crux ...

Tutorial update.

Tutorial di Matita (lupo, capra, cavoli)

Not well understood patch: an assert false did occur, so I changed it to a
pattern matching failure. However, I do not know if this was due to a badly
defined notation or not.

- the confluence of context-senstitive parallel reduction (cpr) is closed!
- the theory of partial unfold on local environments (ltpss) is set up

Matitaweb: Fixed a bug which caused matita to forget the baseuri of the current
script when retracting to the top.

Map in NCicUtils now takes an optional boolea to disable head beta reduction.
We normalize cic terms in the paramodulation blob by stripping out names in
binders.

1) removed many debug prints
2) solved a bug in automation (we had forgotten to saturate clauses in
forward_infer_step, a mistake that prevented equations from being
indexed, resulting in almost certain failure of automation).
3) disabled alpha_eq in NCicBlob.compare, because it now requires a
status containing the correct environment, which can't be guessed
inside compare (enabling alpha_eq results in the automation
sporadically failing).

Matitaweb: disabled many verbose debug prints.

The Blob is not abstracted on the context any more.
The saturate function (that requires the environment now
contained in the status) is now external to the module.
It is defined in NCicBlob.
The functions mk_passive and mk_goals are now expecting
input terms already saturated.

some improvements about the partial unfold on terms (tpss)

Fixes a bug (introduced in the previous revision) which caused the environment
to forget its status.

This commit patches the environment and the library so that their status is
contained in the global status of Matita. This allows several users to execute
concurrently in the same instance of Matita, since they are now using
independent statuses.

File uploading

mah...

The tutorial on line.

The tutorial on line