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.

fixed -debug

moved the expansion of implicits inside the refiner in a lazy way

fixed lapply on new tinycals semantic
removed expand_implicits from elim

fixed some type error

experimental version

new tacticals

ported to new syntactic requirement about terms being surrounded by parens

added iter_option

"better" (????) identification of assertion failures

Debugging code turned off.

dump_moo added

* More profiling code
* Debugging code restructured

Every exception that used to have type string is now a string Lazy.t.

...

readme file

~subst fixed everywhere in the type-checker:
 1. sometimes it was not passed to functions
 2. sometimes it was passed but it was not used/useful/correct
 3. sometimes it was not passed recursively

t renamed to t' since t was already defined in the same file

Bug fixed: the current substitution and metasenv were not propagated to the
check_allowed_sort_elimination function. As a result:
 1. useless metas were opened by the apply tactic
 2. sometimes unification failed

new semantics, should be the basis for the (re-)implementation

Minor fixings.

Tentative title.

Corrected a mistake in power_upto, and decreased the value of just_factor to
three.

definition of eq improved (?) parametrizing an argument

added coercions to Prod

added some comments; general code cleanup

Added basic bibliography.

more comments added

added few proofs

fixed a couple of bugs that broke tests...

few more cases

tlt_defs: notation updated
ac_defs : PREDICATIVE TOPOLOGY: firs attempt

added few cases

fixed bugs in Indexing.find_matches and Saturation.apply_equality_to_goal

fixed some typos

added goals_of_proof

realizability for the induction principle.

added list_concat

added level2 <-> level3 transformations

fixed a bug (status not reset properly between calls), tried some other
euristics (not very satisfactory... :-( )

First draft.

Empty directory.

- added stack frame tagging
- unified "End" for Branch and Select

More informative exceptions raised.

added -nodb support

added support for MATITA_FLAGS and NODB make variables

changed functor interface, now based on proofs instead of metasenvs (this one is implementable on top of ProofEngineTypes ...)

NODB implemented

ignore usual *tex crap

added Makefile

completed instantiatian of level 2 patterns from level 1

bugfix: avoid diversion in "make opt"

- better naming
- uniform handling of empty stack assertion failure
- added Qed and init

first check in of continuationals implementation

in the end: ... proper handling of multiple bindings of the same key, all "set_*" methods now replace the previous binding

bugfix: multiple bindings of the same key work again