"Parallel" rewriting in a list of hypothesis and in the conclusion is now
allowed.

Major code semplification and improvement:
 1. the proof term generated used to have a (Hletin) ...
    Now it has a (H) ...
 2. the code has been greatly simplified by renaming the old variable
    first and doing a letin later; I used to do the letin first and
    rename the new variable at the end

aded a prototype of chtting aboit tacticals

filled disambiguation algorithm section

First draft implementation of rewriting in an hypothesis.
Highly incomplete. Fails randomly if the pattern is not one the tactic is able
to cope with.

New tactic rename (for now for internal usage only).

matita.tex

followed kluwer guidelines

Inizio stesura parte su "libreria tutta visibile".

ported to kluwer style

fixed some stuff in the patterns section

fixed some stuff in pattern section

tests and tests.opt targets greately simplified

added first draft for patterns

predicative subsets started

snapshot

- begin{grafite} environment for script snippets
- more on disambiguation phase

dump_moo.opt

do_test.sh no longer prints the compiler options (used to avoid awk-ing out
the -noprofile flag)

New framework for regression of bad tests.
Now do_test.sh should always return OK if everything is "correct"
(i.e. if good tests are OK and bad tests FAIL with the expected output)

universal quantifier added

The .depend must not be committed! Fixed.

ignore bibtex litter

1. handling of tests and tests.opt targets improved
2. new target cleantests.opt
3. new directory bad_tests with tests that should fail.
   For each test that fails we check if it fails with the expected error
   message.

TODO: the nighlty benchmark could fail to detect the output provided by
the failing tests in the bad_tests directory.

added content level ref

- draft of the first part of disambiguation subsection
- use bibtex

New directory for bad tests with checks on the error message.

...

Debugging code commented out.

Bug fixed: wrong exception was raised (instead of returning false)
when eq_carr-comparing two different things

cic concrete syntax (w/o notation)

better output formatting

removed grammar rule which used to enable things linke "theorem a."

list_uniq abstracted on equality

fixed self and removed more DUMMY... only one left

added print_grammar

removed duplicate entry

tex macros, checked in disambiguation section from whelp paper

dded missing catch for coercions

contribs/PREDICATIVE-TOPOLOGY added as test directory

bugfix, use database name

Introduction, again.:

first draft of db filling script

Introduction (partial).

Introduction.

added an example of reduction of R' and some comments (plus a fix in the demonstration)

Definition of system T.

paper skeleton

Several changes.

A couple more of references.

typos

added Makefile, llncs style, cvsignore

Headings of the matita paper.

Extended bibliography.

Added an example (well founded recursion).

Yet another semantics for simplify.

Yet another semantics for simplify.

fix

fixed inductive types demonstrations

Typos.

CicTypeChecker.AssertFailure now printed.

Debugging code removed.

New syntax for the outtype of a match.

added some stuff on inductive types

Refinement of a Cast was bugged.

AssertFailure from the type-checker now becomes an AssertFailure for the
unifier.

Let-ins with types can now be produced.

Avoid generation of let x = let rec x = ... in x in (x ...).

Let-ins with types can be produced.

Syntactic change:
 [ ... ] match t in t with ==> match t in t return ... with

Syntactic change:
 [ ... ] match t in t with ==> match t in t return ... with

Duplicated exception definition removed (used to give birth to a bug due to
the generativeness of exceptions).

First draft of the introduction.

changed script actions keybindings: s/CTRL-XXX/CTRL-ALT-XXX/

bugfix: no longer raise End_of_file for scripts ending with comments

list sorting (to be completed ...)

added tail function

added bool_elim (elimination which preserves infos on the eliminated value)

since the outtype is now refined correclty some types can be opmitted

refined outtype used to be discharged

matita*.opt are now considered as if they were matita*

make profiler silent

added calbback to make the profiler silent

added support for ALT-L expansion of tex macros

ligature expansion now considers also tex macros

exported is_blank

added ligatures expansion support functions

added support for expansion of ligatures ALT-L will trigger it

better distinction of (* *) and (** *) comments
- first kind of comments is thrown away by the lexer, still admitting comment nesting
- second kind of comment is lexed as usual returning "BEGINCOMMENT" .... "ENDCOMMENT" token stream

avoid losing work on CTRL-N

removed no longer needed dependency on pxp

fixed typo

more structured makefile

"towards a distribution of matita" changes:
- @USER_HOME@, @USER_NAME@ no longer hard coded at configure time
- added support for tilde expansion in configuration file
- added support for runtime overriding of RT_BASE_DIR
- better configure.ac, can now configure RT_BASE_DIR, debugging, and distribution defaults

added tilde_expansion of directory settings

added char functions:
- is_alpha, is_digit, is_alphanum
added string function:
- tilde_expand

changed stack entry representation

Bug fix: index.theory dereferentiation works also for exists and resolve.

Semantic change: I always consider a type with no constructors as an empty
type even if it is mutually recursive with non-empty types. I think that
this should be a sound generalization.

Note: Coq assumes a type to be empty iff it is not mutually recursive with
any other inductive type.

Semantic change: elimination of a term whose type is defined in a block of
mutual inductive empty types