Tests enabled again.

:-(
This commit introduces an hack in deannotate.ml to compute on-the-fly the types
for the body in a LetIn parsed from an XML file. This happens when parsing Coq
files. We should re-export everything from Coq sooner or later.

New version of freescale:
 a) bug fixed for SBC, JUMP e JSR
 b) medium_tests theorems ported to new pattern syntax
 c) new test for a perfect number generator
 d) "lambda-delifting" of let rec reverted (waiting for a better
    implementation of simplify or for the new generation kernel)

Problem solved (was: apply needed an argument to avoid a great slow down due to
conversion of a meta-open and a meta-closed term).

Almost always correct optimization: during unification, a meta-closed term and
a term that is not meta closed are not tried for convertibility. This greatly
speeds up, for instance, some examples in Bertrand.

fixed implicit

Nuova dimostrazione riflessiva di le_to_Bertrand.

if -debug is specified do not catch all exceptions

Very experimental commit: the type of the source is now required in LetIns
and Defs. This is a back-porting from the new generation kernel.

TODO:
a) debug some failing examples (paramodulation)
b) port the code by Ferruccio
c) do something for Coq files (that are now rejected)

fixed wrong dependencies in debian package reported by oliboni

Bad hack to avoid failure of conversion (unfolding) in "unfold t in H" where
H is a definition. In this case it is perfectly normal that t may not occur
in the type or in the body of H.

...

Scripts fixed because of:
a) reduce got rid of
b) different behaviour of reduction w.r.t. zeta-reduction

Tactic reduce got rid of. Use normalize, instead.
Rationale: the two tactics did the very same thing, but normalizes exploits
reduction machines and so it is really faster in many cases.

whd: ~delta=false now controls also zeta-reduction. This greatly speed-ups
some operations when definitions are in the context.
Moreover, the semantics seems more reasonable (????).

An unimplemented case of clearbody is now implemented.

check_metasenv_consistency:
big ad-hoc performance improvement propagated from CicTypeChecker to CicRefine.
This really cuts down the total refinement time in some situations (freescale).

Example query fixed.

Debugging print removed.

Added ad-hoc optimization for check_metasenv_consistency, case Rel to Let-in
vs Def. Rationale: this is the case of an IRL when the metavariable is
created in a context with definitions. Without this optimization, a (possibly
expensive) reduction is always triggered.

Note: this should be better handled using a reduction strategy based on
heights.

Performance improvement: let-ins should always be pushed to the context with
their type (to avoid multiple re-typing).

Scripts fixed. They were broken since the change to the behaviour of CicMetaSubst.delift w.r.t. definitions in the context.

LAMBDA-TYPES: some more generation lemmas and some proofs improved

Potentially (and, at least sometimes, actually) big performance improvement:
let-in were always zeta-expanded during delifting. As a result, implicit,
in a context with definitions, were always refined with a type that was well
typed, but only up to (potentially expensive) reduction!

Redundant check (because of an invariant) removed.
The check was added by Tassi when adding universe constraints.
However, it is now believed to be useless.

* please let the library in shape *

fixed

skipped freescale and dama_didactic

fixed deps

reworked freescale stuff to put \m as a left parameter

no more assembly/ to skip

fix typo

added mkdir

...

some corrections and additions

from now on, export MATITA_EXTRACT=true to extract

verbosity increased in case of error

components/library: dotdothack removed
legacy & LAMBDA-TYPES support $(MATITAUSEROPTIONS) (= -system for fguidi)
LAMBDA-TYPES: two missing generation lemmas added

New syntax for patterns.

prodT ==> prod

A) New version.
B) set "baseuri" removed
C) minor clean-up

we added the classic substitution function

firs attempt to compile with ocamlbuild

the proof of bertrand's conjecture is now complete

I added some debugging information

added MATITAOPTIONS -onepass as for LAMBDA-TYPES

LAMBDA-TYPES: added wf3 (legal context predicate);
              Unified-Sub removed because of its early stage

$(H) added :)

LAMBDA-TYPES: dependences calculation improved

LAMBDA-TYPES:
we introduced incremental dependences build to speed up the compilation
dependences are now dynamic so the file "depends" was removed from svn

- added some options to matitadep: -stdout and -exclude
- LAMBDA-TYPES: improved Makefile, Base-2/theory.mma is no longer needed

sieve of erathostene (proof of soundness almost done)

A new very simple example for recursive functions. Still bugged, but getting
better.

Avoid translating back recursive fixes to the same URI.

Avoid application to 0 arguments.

Better handling of exceptions.

svn:ignores fixed

-onepass option removed from Makefile to comile Base-2/ext/arith.ma ???

LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES
some additions and redundant dependences fixed

splat_args is now better understood and debugged: we need TWO splat_args, one when
the term is a Rel (that skips the bound variables) and one when the term is a Fix
(that passes bound variables around).

added small test, fixed some bugs

many fixed in translation functions

dependences needed a fix :)

we are moving the devel root one dir level up

...

snapshot inverse tranformation

transformation almost finisced, not tested

now inline "file.ma" is allowed.
file.ma must be compiled and all its contents are inlined

Added o.ma (some results about the magnitude of functions *)

initial steps of convertibility

some bits of reduction, reusing psubst

Complete proof of Bertrand for n >= 256.
Removed the baseuri form all files in nat.

Prima versione di bertrand. Tanti cambiamenti qua e la.

baseuris removed from files

fixed dependences

conversion half inplemented

renaming

reordered cases

reorganization of sources

substituion and lifting implemented

renaming

factorized common components of objects

added Local pragma, moved leftno and inductive into obj, added relevance attribute of parameters

added leftno to indtypes, better indentation and comments

nCic almost finished

renaming

regeneration with new results

fixed path for matitadep

fixed make dist

better error message in case inclusion failed

allow to use "../foo/bar.ma" as a path for the include statement

progress.

A formalization of modified realisability with truth as in
``Internalising modified realisability in constructive type theory'',
Erik Palmgren, Logical Methods in Computer Science, Vol 1. (2:2), 2005, pp 1--7.

Bug fixed in generation of elimination principles of inductive types having
at least one constructor of type (A -> i) -> i that was not the last
constructor.

prodT merged with prod
fstT merged with fst
sndT merged with fst

ProdT was a perfect copy of Prod. Removed.
Sum is now in Type.

Results about Chebyshev teta function.

cic defined (half)

Some more theorems.

reindent