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

missing mlis

better dependencies among modules and symlinking of several matitatools to a single one in order to reduce global size of matita executables

added documentation on allowed eliminations

1. a simplified version of check_allowed_sort_elimination is now exported
   from CicTypeChecker to be used in CicElim :-|
2. check_allowed_sort_elimination fixed w.r.t. the case Prop unit vs *

Euler totient function is multiplicative!

More exceptions pretty printed.

Major code semplification in check_allowed_sort_elimination: the
need_dummy and not need_dummy cases are now unified.

Unfinished proof commented out.

Proof of unicity of proofs for:
 1. decidable equalities
 2. P x = true for some function P

enable static linking of executables (try "make static")

rebuilt

added gcc lib dir for enable static linking of libstdc++

Maybe this time we will be lucky.

() around tactic terms

Totient function and related files.

matita distribution stuff

fix

Bugs fixed.

Aczel categories finished
quantification domains started

Bug fixed: the wrong mark was chosen for yesterday.

Ported to multiple marks in the same day: today newest mark is compared
with yesterday newest mark.

New "global performances" bench (for native code).

1. syntax error fixed
2. r.e. for the time format fixed

sql query fixed

Better detection of spurious status lines.

Mark fixed.

fix

fix

New format for benches (with much more precision).

fix

fix

1. Parameter enable (default true) added to HExtlib.profile
2. profiling code commented out in cicReduction since it affects performances
   very badly

...

typing errors

added constraing on non-empty context for tactic application

improved Makefile

Dead code removed.

Parentheses must now be put in patterns like in tactic arguments.

Semantic change: applying a tactic to the empty goal list is now an error.

Syntax change:
 1. hypotheses patterns are now separated by spaces (they used to be separated
    by ";")
 2. terms in patterns must now be put in parentheses like tactic arguments

ProofEngineTypes.Fail printed correctly.