disabled coercions when refining paramod proofs (attemt to understand the slowdown of night-tests)

fixed propagation under Fix/Lambda/Case of coercions, better names are
generated.

there is still a question for CSC about the context of the metavariables opened
by example 51 that seems too long.

code still needs some refactoring, auxiliary functions are ready to be
lambdalifet out.

potential slowdown: The coerce_atom_to_something now looks for the *best*
coercion, where best means the one that opens the least number of metas.

Some simplifications.

coercions under Fix and Case. Code refactoring needed

added a duplicated implementation of replace lifting

...

- lybrarySync:
  patched generation of published xml files: inner_sorts were not considered
- natitaInit:
  patched configuration parsing priority

- matitaInit matitaprover matitadep matitamake:
  fixed configuration precedence:
  cmdline > configuration_file > default
- core_natation:
  added notation for single step parallel reduction: =>
- LAMBDA-TYPES: some new theorems
- LOGIC: some new definitions

added fix case

coercions are propagated under Fix (but not mutually recursive Fixes)

Dandling ")" removed from notation for 'exists.

Composition of coercions with arity > 0 is now implemented correctly.

A test for propagation of coercions (that open new goals) under lambdas,
cases, etc.

1. composition of coercions with saturations > 0 is now implemented
2. as a side effect, there is no longer any difference between composition
   of coercions and the compose tactic

TODO: composition of coercions having arity > 0 is not implemented yet

alpha conversion to avoid case-insensitivity of MySql on my laptop.
OK, I know, I should fix it...

baseuri changed

fixed coercions between arrows when the arrow is dependent.

captured exception preserved (was replaced blindly with a RefineFailure)

reverted assertion, since it may happen to look for a coercion to funclass
even outside fix_arity (in cicRefine/eat_prods)

refactoring of all coercions code and add a check to not perform a coercion check if it is not needed

bugfix in computation of src and tgt for coercions with arity > 0

tests for coercions under lambdas

Coercions are now generalized to the general form
f: \forall xs:Ts. \forall a:A xs. \forall ys:Ts'. B xs a ys
where f is declared as a coercion from A ? to B ? ? ? using the syntax

   coercion uri arity saturations

where:
 1. arity and saturations are optional with default 0
 2. the saturations option is the number of ys

Useful example: it is now possible to declare a coercion from
 nat to \exists n:nat. 0 \leq n
obtaining something extremely close to Russel (the new implementation of
the Program tactic of Coq) up to the fact that coercions are not propagated
yet under mutcases and fixes.

TODO: composition of coercions having saturations <> 0 is not implemented
yet (but should be easy to do, at least on paper)

Coercions rework:
- new functions:
  - coerce_to_sort
  - coerce_to_something
  - coerce_atom_to_something
- added call in Cast
- coerce_to_something goes under lambdas in both
  variant and contravarian positions, to if there are
  c1: B -> B1 and c2:A1 -> C coercions, you can cast a function
  f: A -> B to A1 -> B1.

coercions from funclass are not supported

...

bla bla bla fallback

added a binch of svn:ignore

add a fallback in case the binaries are in the path and not in the runtime base dir

print few more wired assertions

the version on the livecd

more stuff to reach an intensional definition of finite sets

added an utility function

0.2.0

* definition of implication free propositional formulas
* definition of a classical semantics
* proofs of correctness of some syntactical manipulations to reach
  normal forms
* definition of sequent calculus trees
* proof of soundness of sequent calculus derivations
* proof of completeness of sequent calculus derivations (unfinished)

A primer for Matita with some easy, medium, difficult and impossible exercises.

We define proof tree tracks and normal proof tree tracks separately

refactoring

proof by "introduction" (impi) implemented in full

thread-based interface activated again

Bug fixed: RewriteLR were not recognized correctly. Moreover they were also
handled incorrectly (according to the is_top_down flag that should be irrelevant).

Bug fixed: the initial metasenv used in the two tactic was empty!

Avoid reusing Hbeta several times.

select now works correctly even if multiple hypotheses with the same name are
present in the context.

Avoid confusion for names of proofs put in the applicative context.

"obtain H E1=E2 by proof" is now working

little change to theorem eq_gcd_times_times_eqv_times_gcd

removed generic_sigma_p since generic_iter_p is the same

something was really too slow...

default equality stuff filtered out from hint rewrite

removed comments in proof presentation

renamed generic_sigma_p.ma to generic_iter_p.ma

added 'rewrite' option to the the hint macro. a cicBrowser with all library
objects that may rewrite the goal is displayed.

We add a binary for computing the "heights" of helm objects
[this is related to the height of the dependece tree]

added development path normalization, inclusions with '../' in the path should now be handled correclty

auto -> autobatch

Some notation added

more stuff about coercions

little bug in coercion generation found. it use to create more coercions that expected (luckily convertible).

makefiles updated

makefile updated

matitac: We do not generate the .moo and .lexicon of a dumped .mma
Base-2 : makefile patched

added some notation

added another example in which our coercions are powerful

used ;try assumption instead of .try assumption

; and not . after auto-paramodulation

reverted previous fix

restored compaction of metas at the end of given_clause

Makefile missing in previous commit

New developement LOGIC about the cut elimination of implication for Sambin's basic logic; one of the rules must be corrected (work is in progress)

added test about dependent coercions

Prototype of min_aux changed.
Now (min_aux off n f) find the smallest i such that
* f i = true or i = n+off
* \forall j,  n <= j <= n+off,  f j = false

The new function does no longer compute with off. Thus we obtain
for free a great computational speed-up in every function defined
in terms of it.

auto vs autobatch fixed

autobatch parameters reajusted

fixed makefiles to make it compile cleanly again

Procedural: the statement body and it inner types must satisfy the Barendregt
            convenction on bound variables

Another nicer version.

Even nicer script.

The nicest script obtained so far.
What is left, is a bunch of change/normalize/whd/simplify that are difficult
to control precisely.

acic_procedural: bug fix:
                 sometimes whd is not enough, we need normalize ...

More simplification due to the new conversion strategy.

Script simplification due to the new efficient conversion strategy.

Tentative bug fix for diverging pretty-printing function.

Initialization of matita.map_unicode_to_tex moved from matitaGui to matitaInit
(so that ocamlc now works again).

cicUtil        : new test function "is_sober" to test the integrity of a term
                 now fails when fake applications are detected
acic_procedural: some bug fix

Convertibility now converts machines in place of terms.
Actually, the heads of the machines (i.e. everything but the stack) are
still unwinded and converted as terms. Thus there is much space for
improvement.

map_unicode_to_tex is no longer optional and it always refers to the current
user choice.

paste_unicode_as_tex is now false by default; moreover the flag is used
everywhere (but in patterns, I do not know why)

COERCIONS: tentative addition of an equivalence relation over coercion source
carriers (convertibility) for the moment used only in the FunClass case.

the cade was escaping the table name and not the uri

fixed escaping for sqlite

fixed an escaping error, added more infos to the generic error, callback catches and prints exceptions

Typo fixed.

Super-nice notation for the assembly stuff.

the predicate for elim was not built correctly when more than one right parameter was found

recursive argument in let rec is not printed explicitly.
I let to ferruccio optimize the case in which there is only one argument or the recno is 0 and thus can be omitted

fixed coercion graph print, moved coercion graph and auto gui to the view menu, added a mini test about coercions

added missing parenthesis

fixed includes and added notation for bytes

More lemmas.