returns_a_counductive implemented

type_of_branch ported and optimized to not lift the outty every Prod, keep the
number of passes binders and lift it just once

is_really_smaller ported, still to understand the case in which
whe find a Fix or and applied Fix (still there after a whd)

debujin implemented with the map recursor

bug found rewriting the kernel backported: n instead of m when pulling a def from the context, previously a meaningless index was used

non debruijned constructor may be useless elswere, for the moment we do not bind it

guarded_by_destructor ported, many auxiliary functions still to be done

removed FSF banner

added ugly test showing many many bugs in the current kernel

added slim version of does_not_occur

added translation of Set to Type0 (avoid warning)

fixes backported from the new kernel

removed dummy rewrite

removed dummy rewrite

removed dummy rewrites

fixed according to the new rewrite semantics (fails if no progress)

fixed depends after the removal of Fsub

better check for progress

typeof_obj0 implemented

1) added get_checked_indtys that returns the whole block of inductive types
2) type checking of Match almost finished

progress made better, still not perfect

added to rewrite a check to effectively do something, and fail if nothing has been rewritten.

added some comments, but the samentics of many functions is still unclear to me

added set_ppterm

Automatic generation of elimination and inversion principles for co-inductive
types disabled (since it does not make sense!)

Large amount of duplicated code (still in comments) factorized.

1) Impredicative sort "Set" removed everywhere.
2) Sort "CProp" is now predicative.
3) Optimized case IRL in check_metasenv_consistency.

1) more sharing everywhere in NCicSubstitution
2) type of iterators in nCicUtils changed to take a NCic.hypothesis when
   crossing binders

more cases of the type checker honoured, still missing Match and Const.
lookup_meta added

added is_closed to nCicUtils.
partial implementation of the typeof main function.
dummy nCicPp waiting for a proper replacement

moved psubst and list to the new iterators, result not very impressing
from the #lines point of view

added iterators over NCic terms

removed FSF header

Updated depedencies.

insert comments of old tpechecker

Reorganization of list library (step 1)

new are_convertible and head_beta_reduce

context for fixpoint body created in the hopefully right order

ported to the Cic LetIn with explicit type

this patch is a shit, the part that fixes the heuristic about Obj.magic should be really adopted, the rest is metaocaml specific

fix with m (to be optimized) are rewritten such that m is abtracted outside the fix

very very interesting hack

small update

argument of type mcu_type always abstracted first

XXX this is the beginning of the metaocaml work XXX

Fsub moved in contribs

cicNotationPp: fixed letin syntax (now typeless)
LambdaTypes: typeles letin syntax, some notational changes, Makefile fixed

since many stuff is under contrib, we need to ignore less directories

library_auto moved inside contrib, still not ported to the relatively-new
build system

moved dama/ and dama_didactic/ in contribs/dama/
the tests output should not change and history is preserved

freescale moved under contribs. contribs made relocatable
since all internal Makefile include a Makefile.defs defining
where to find matita*
tests should not be affected since the output of the compilation is
the same and the URIs are the same

New syntax for auto-related tactics and conclude/obtain.

Script fixed (it did not compile due to a mistake before committing).

Base-2 is not compiling properly and is excluded for now

changed auto_tac params type and all derivate tactics like applyS and
demodulate honors the same syntax.

new syntax for auto parameters:
  auto string-params by only_terms_to_use
new syntax for declarative eq chains:
  [(conclude|obtain H) t1] = t2 (auto-params|exact t|using t|proof)
  exact t : apply t
  using t : 1 demodulation step using t
  auto-params : first [ auto ; auto paramodulation ]
  proof : id_tac
manual still to be updated

new semantics for 'by t'

removed pointless test

I believe that auto paramodulation does not try to
saturate guarded equations and solve hypothesis with auto...

added library option to auto

letins are no more unfolded, we do that by hand

letin are no longer unfolded thus coercions not propagated deeply.
workaround not using letins

End of patch for computation of LetIn types. Now types of mutually (co)recursive
function are added to the environment _after_ Implicit have been resolved.

Bug: types and terms pushed into the context must be Implicit free.
Partial fix committed (types of Fix and CoFix not patched yet).

-debug improved

...

prerr_endline => debug_print

prerr_endline => debug_print

Number notation for Coq is back again, waiting for the ultimate solution.
Idea: raise the right exception when the Uri is not found.

Files committed by Enrico (a mistake, I suppose) removed.

Procedural  : added some missing cases
LAMBDA-TYPES: improved preambles

LAMBDA-TYPES: level 2 dependences are now correct, at least :)

Procedural  : tentative update to the new letin cic construction
LAMBDA-TYPES: level 1 is stand alone instead of coq dependent
              level 2 is untested so will not compile for now :)
legacy      : unpublished

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