Matitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping.
Added pretty-printing of unhandled NTacStatus.Error exceptions.

refactoring ...

-- some renaming in basic_2

old pr2_subst1 (Basic-1) closed!

Matitaweb: first attempt at web UI for disambiguation.
Also includes a rather radical change in the way the graphical layout is
handled.

Now it should compile :-)

Optimization. Check removed.

Disabled debug.

1. ported to camlp5
2. added a boolean to qed to governe indexing
   the syntax for disabling indexing is "qed-"

typos

We order alternatives according to the number of subgoals they open.

QED takes a boolean parameter governing indexing.
Syntax to avoid indexing is qed-

Alternatives are ordered according to the number of subgoals
they generate.

JMeq lifted to work on Type[1].

Removed some unneeded normalizations from the generation of discrimination
principles (they had a bad effect on performance).

Matitaweb: added preliminary support for interactive disambiguation.
Ambiguous expressions are reported to the client and highlighted.
The possible interpretations are shown in stderr.

Matitaweb: added a function MatitaAuthentication.get_users returning
the list of the registered users.

- the relocation properties of cpr are closed!
- the support for global references is started ...
- some refactoring.

commit by user andrea

commit by user andrea

commit by user andrea

Localization of errors.

Changes in "destruct" tactic (allowing performance improvements):
1) discrimination principles are now generated upon definition of an inductive
   type I and recorded as objects I_discr and I_jmdiscr (resp. leibniz and john
   major's principles); in case JMeq wasn't loaded at that time, it is possible
   to explicitly request the definition by means of the command

   discriminator I.

2) destruct uses the aforementioned principle rather than generating a cut at
   each discrimination step

3) destruct performs generalizations using the basic generalize0_tac, rather
   than generalize_tac: this should bring small performance improvements.

compact coercion command: "coercion foo."

commit by user andrea

commit by user andrea

commit by user andrea

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.