Optimizer: refactored according to its formal description

Serious bug fixed: a variable was captured during unfolding of Fix, resulting
in the context of the return type of mutually recursive definitions being
lifted for each function but the first one!

added eta expansion to avoid universe inconsistency.

Several instances of the same bug fixed at once: when processing a Fix,
before adding the types to the context (to process the bodies), the types
must be lifted. The simplify tactic is still not working propertly.

Debugging code removed.

elim tactic: it needs two arguments, a term as well as a pattern
CicReduction: head_beta_reduce now can take the number of beta-redexes to reduce
Procedural: refactoring

New contrib moebius.ma.

Extensions required for the moebius function (in Z).

Role of
 - replace
 - replace_lifting
 - replace_lifting_csc
clarified with comments. None of this function is the inverse of subst :-)

elim tactic: now takes a pattern instead of just a term
             works as before for now. the pattern wil be activated soon
Procedural:  cleaning up
ProofEngineReduction: new subst_inv function exactly inverts subst

Few theorems added.`

new version of div_and_mod

Capturing Invalid_argument inside pp (otherwise we cannot even
see what's wrong *) wrong.

case to elim conversion works fine

added a test for rewrite under Pi

rewrite tactic: bug fix in rewriting under Pi's:
                the application context of the subterm to rewrite can not be
forgotten

Procedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation

some improvements

Procedural: bug fix

Relational: one file was missing :-)
Procedural: the cic object preprocessor was not added to svn :-)

Procedural  : cic object preprocessor added
depend[.opt]: some fixes

Procedural: now patterns for rewrite are generated correctly

Procedural: some improvements
rewrite tactic: bug fix in hyps searching
TermContentPres: one space added in let-in rendering
prova.ma: new procedural proof of ty3_gen_cast

procedural proof of ty3_gen_cast

"by j let x : T such that P(x)" generalized to allow arbitrary justifications.
The code and behaviour should be cleaned up a little bit.

some improvements

- Procedural: some improvements
- intros n tactic: now tries whd when Pi or let-ins are not enough

decompose: delta-expansion of the type to eliminate now works fine

RELATIONAL: new undecomposable definition of NLE
Procedural: some refactoring
decompose tactic: only types of sort Prop are decomposed now

decompose now works without premises

procedural      : some improvements.
decompose tactic: user provided premise and types removed.
                  The decomposable types are now the non-recursive inductive
  types without right parameters and are auto-detected

acic_procedural: changed module compilation order
TermAcicContent: bug fix in AMutCase
                 the presence of left parametes was not taken into account

small fix to make it compile again

added some code to print the praamodulation proofs with a graph

Unified-Sub: lift_comm completed

contribs: some improvements

contribs: some improvements
Sequent2pres: added some spaces

refactoring

some improvements

Procedural       : some improvements
PrimitiveTactics : tentative implementation of using clause in elim
CicNotationParser: noe declarations of the form (_:t) are parsable

LexiconAstPp: fixed syntax for include
TermContentPres: fixed syntax for letin
lexiconEngine: moved callback from grafiteParser
matitac: -dump patched

unified: some theorems on Lift started

Unified: INC and BEq removed
contribs: added dependence to ../legacy in the Makefile

added option -dump to matitac for persistent macro expansion

Avoid generating invalid names with "'" in the middle of them.

Added toggle for enabling/disabling the conversion from multibyte unicode
characters to TeX when converting CIC terms to textual formulae. The toggle is
under the Edit menu (rational: it's near the paste commands, maybe it should be
added to the GtkSourceView contextual menu too). The toggle governs the
matita.paste_unicode_as_tex boolean registry value. The txt_of_* rendering
functions have been changed to accept a new optional boolean parameter.

The ApplyTransformation.txt_of_term function has been made more robust to
exceptions.

- moved to the view menu toggles for coercion hiding and notation pp
- moved back the high level pp toggle to the debug menu

Exceptions should never escape the final exception handler for the worker
threads. This patch just reduces the probability.

Debugging code fixed. To enable debugging just set debug to true at the
top of the file.

Debugging code removed.

moved the high level pretty printing setting to a toggle menu item of the View menu (with CTRL-P shortcut)

More progress in technicalities/setoids.ma.
I have now reached the final theorem!

Manual for the "default" command updated.

* 'default "equality"' command changed to consider also
  eq_rec, eq_rec_r, eq_rect, eq_rect_r
* rewrite tactic changed to rewrite also in goals of type Set and Type
* more progress in technicalities/setoids.ma

If a pretty printed term spans on multiple lines, then it is printed after
a new line and followed by a new line too.

Important commit:
from now on the pretty printer CicMetaSubst.ppterm_in_context is substituted
with a reference to an high level pretty-printer (now defined in
matita/applyTransformation.ml). In the debug menu there is a switch to turn
it off and get back the old pretty-printer.

developments fixup

Unified refactored

definitions fixup

fix dependences for matita

LAMBDA-TYPES: refactored

refactoring

Level-1 refactored

refactoring

refactoring

New dependency over acic_procedural.

- Procedural: moved in a directory on its own
- ApplyTransofrmation: now handles inline macro expansion
- GrafiteParser MatitaEngine MatitacLib: added a callback in each
- tests/letrecand.ma: changed baseuri

More stuff in technicalities/setoids.ma

Debugging deactivated.

Bug fixed in the computation of the disambiguation domain of a let...rec.

Incredible bug fixed in Fix and CoFix. The types of the mutual inductive
functions were not lifted when added to the context.

Second formulation of a constructive (positive) proof of Lebesgue's
integration theorem, based on a proof by Weber.

Serious bug fixed: the types of a real mutual fix definition were not lifted
as required. Moreover, an unification exception used to escape the refiner.
Now it does no more, but the error is not localized (being about the branch
of a MutCase that has no precise localization).

added preamble file in LambdaDelta and improved theory files

The baseuris changed

Level-1: regenerated with differnt baseuris

restored coercions between eq and eq

reverted a commented substitution in build_newgoal, added an euristic to
order the lambdas of a proof abstracted in a letin such that dependency betwwen the types of the lambdas is inferrable by the refiner

methods eos, goto, advance and retract now catch Invalid_argument "Array.make"
that is raised when the script is too big to be handled (this makes quit work!)

Several bugs fixed:
 1. mutual definitions were not generated correctly
    (e.g. let rec even ... and odd in even actually resulted in a
     definition of odd!)
 2. a top-level mutual definition now generates two constants (as it
    should have always been)

New test for mutual recursive definitions.

Proof size nicely reduced using distributive branching with goal selector.
Look for
 ] ;
 [1,3,5,7,9,11:
   ...
 |2,4,6,8,10,12:
   ...
 ]

Even more (painful) work on setoids.

Behaviour of CicRefine.type_of_aux' on MutCases changed: branches are now
processed from right to left to make the cases tactic open goals in the
expected order.

More work on setoids.

Some more datatypes lifted to Type.

well-formed ocamldoc comment

preliminary cookie support

Added option datatype. Required (for technicalities/Setoids.ma).

"Warning/error/debug/infos" messages now sent on stderr.

Some changes:
1. error messages are now in HTML (they used to be in plain text + vt100 colour
   scheme)
2. commands are now expected to be in a fragment of the pgip protocol.
   Supported commands are:
    <pgip><doitem>...</doitem></pgip>
    <pgip><undoitem>...</undoitem></pgip>
3. the terminator sent back is now preceded by either -1 (command not
   successful) or n (an integer to be sent for undoing)
4. undoing is now supported

tactics.mli: regenerated
LambdaDelta: regenerated with some new theorems

matitaGui: some missing cases during disambiguation now treated
grafiteAst: rename tactic removed
procedural: some improvements

send internally generated headers in lowercase form for consistency

some patches

Just a few lines test to understand with Cezary Kalinsky how much effort is
required to integrate Matita in his generic AJAX based interface.
matitawiki is an executable that reads from stdin and prints output and error on
stdout/stderr (both followed by (Char.chr 249) after each command).
All the interactive commands (thus also "undo") are not supported.

Bug fixed: if the context of a sequent was empty a vertical box without content
was generated. This is not allowed by BoxPp (assert failure).

Added new function txt_of_cic_sequent.

1. buf fixed in eval_from_stream when first_statemente_only=true:
   the last computed states were lost
2. added a new watcher function to eval_from_stream.
   The function is called after the execution of each command.