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.

An "assert false" used to be raised when matitac was started on an empty file.

some updates

Unified: refactoring

Unified: refactoring

Unified refactoring

Unified: refactoring

new version, using new tacticals

This is the roadmap of the constructive proof of Lebesgue's dominated
convergence theorem in the order theoretic setting. I.e. we speak of
convergence (in terms of liminf and limsup) and not of norms/measures.

The formulation should be fully constructive:
 1. the exceeds relation is used in place of the derived negative notion
    <= for partial orders
 2. strong sup and infs are used in place of the weaker sup and infs
 3. the statement of Lebesgue's dominated converge theorem is just
    extensionality of the functional
      \lambda f. liminf f a_n
    with respect to the apartness relation # over real numbers and the
    exceeds/apartness relation over partial orders.

Interesting points to be noticed:
 a) one lemma used in the proof is Fatou. This lemma can be given in the
    usual negative formulation (i.e. on <=)
 b) another lemma used in the proof is that the liminf is less or equal to
    the limsup. This lemm can be given in the usual negative formulation
    (i.e. on <=). Moreover, we feel that if <= is not defined as
    ~< it is actually impossible to constructively prove it.

CoRN (new version) has been committed by Andrea in library/algebra/CoRN.

Added SetoidInc.m

Some CoRN files.

procedural: added fwd rewrite in arbitrary proofs (not just premises)
            added whd conversion before intros when needed
prova.ma  : highlighted a bug with the "in" clause of the "match" constr.

procedural: buggy ast renderer fixed

attributes now in the proof status: commit 4

attributes now in the proof status: commit 3

attributes now in the proof status: commit 2

attributes now in the proof status: commit 1

Porting of setoids.ma from Coq continued.
The fact that simplification does not work properly slows down the whole
process.

Bug fixed in definition of cic:/.../setoids/make_compatibility_goal_aux.con:
two generalizes were done in the wrong order, permuting the arguments and
making every relation change its variance!

- inside dicrimination_tree is now checked the invariant that bad terms are indexed, but this invariant is not always respected, so a 'Dead' representative is used and a warning is printed.
- autoCache (should) not index bad terms

;auto fixed

removed debugging printing

debuggin message improved

add_moo_content does not add a coercion statement twice

Added check for duplicate (convertible) composite coercions,
that are not added anymore.
Nicer api for meets used by unification.

Erroneously declared coercion removed

ready for ocamlnet 2.2

more elegant handling of all/opt building

Notation is finally fully working everywhere.
What a great day!

Debugging code removed.

Riesz_spaces are now seen as lattices + vector spaces + ordered abelian groups.

oder tests

There used to be two minimal joins between an ordered_set and an abelian_group:
ordered_field_ch0 and riesz_space. To avoid the problem without introducing
backtracking in unification I have introduced ordered_abelian_groups.
An ordered_field_ch0 is recast as a field that is also an ordered_abelian_group
and a cotransitively_ordered_set. I still have to recast riesz_spaces as
vector spaces that are also ordered_abelian_groups and lattices.

Same fix of the previous commit, but in a different case.

1. More debugging code
2. "Bug" "fixed": when the pullback of two coercions is computed, only the
   join is returned, but not the two coercions that complete the pullback.
   Thus we need to recompute them and it may happen that we find more than one
   parallel coercions. This "fix" just randomly picks the first one (instead
   of raising an assert false). All this stuff must be handled in a better way.

added oblivion_universe and used it in paxck_coercions

some tests patched

Some more notation can now be used.
However, in integration_algebras.ma there are several situations where
multiple meets are found and notation cannot be used.

le x y ==> x \leq y  (now possible because of a bug fix in coercion
serialization in .moo files)

Serious bug fixed: arities of coercions in the .moo files were not computed
correctly. Thus including another file a bugged coercion graph was produced,
with randomic effects quite hard to understand. (Examples in dama where
it was not possible to use <= in place of le here and there because of a
coercion with the wrong arity).

 dependence to legacy/coq.ma fixed

now we try two distinct depend files for compilation in byte and native code

Record with simulated manifest types are now used everywhere in
integration_algebras.ma. They seem to work really very well (up to missing
but due syntactic sugar).

First attempt at using/simulating records with manifest types to encode
mathematical structures that form a DAG. So far it works quite well,
but the generation of the "coerced" projection should be automated.
Something to write a paper on.

eq_ind' generalized to eq_rect'

- tactics:
  rename tactic enabled,
  rewrite and rewrite_simpl now take optional names for the rewrited premises
- procedural script reconstruction
  now starts directly from acic bypassing the content level,
  the script for the use case proof in matita/contribs/prova.ma is reconstructed  completely now and is correctly parsed and typechecked

Yet another localization error in eat_prods fixed.
However, the fix is very very ugly (it uses unsharing) and clearly shows
a source of inefficiency (and possibly also divergence, I would say).

.depends committed to fix non-compilation errors

some depend files

legacy development created

- sc3/props.ma sc3/arity.ma: dependences fixed
- csubc/arity.ma csubc/csuba.ma: reverted as no fix was needed

Add_moo_content modified to avoid repetitions of index command during inclusion.

Minor change.

Collapse_head_metas transforms all terms "not-recongnized" into a
meta.

In the let-in case we compute the type and add it to the context.
Before it was computed every time

The function uri_of_term now works also if the explciit substitution list
is not empty.

Speeedup! (by caching)
The costing operation is baseuri_of_file that parses the whole maybe big file to extract the first command line.

added some missing includes

New declarative tactic "we proceed by cases on t to prove t'".
Very unsatisfactory since it already introduces the hypothesis in advance,
actually ignoring the following "case S (n:nat)" declarative command.
I do not see any easy solution at all.

Bug fixed in cases (it did not produced the right number of lambdas for the
outtype of dependent inductive types).

Tactic cases documented

New tactic cases (still to be documented).
It is necessary for the declarative language and it is useful anyway.

Procedural: method "Apply" ok in forward style

Procedural:   "ByInduction" method ok
GrafiteAstPp: letin tactic now works

An idea to implement manifest record fields:
record r : R := { c1 : T1 ; c2 : T2 with f c1 = g c2 }.

Only the syntactic sugar is actually missing!

Procedural: some improvements

M    logic/coimplication.ma

Renamed iterative into map_iter_p and moved around a few theorems.

Proof of Euler theorem.

Up to definition of limsup as liminf computed on the reverse ordering.
However, I am no longer sure that this is the best way to proceed since
the lemmas to be proved are a lot and the typing is difficult. However,
this work should be done anyway to state limsup f x = - liminf f (-x)
that we need anyway.

Fatou lemma achieved (up to a few more axioms here and there...)

Huge DAMA update:
 1. up to Fatou lemma (almost there)
 2. requires the new unification procedure for coercions to enable
    multiple coercion paths between two nodes
 3. it stresses CicUniv.mere_ugraphs. To compile the new DAMA file quickly
    you have to disable that function :-(

Bugged code patched, but not in the optimal way.
The problem is that in two different interpretations a symbol id can be
interpreted as dsc in different locations. Using the previous code it
happened that every interpretation was pruned out since a symbol id occurred
twice (in different locations) in an/every interpretation. Now the couples
(loc,id) are considered for disambiguating between the two interpretations.
However, this way we hide information to the user (what other occurrences of
the same symbol are given the same interpretation).

Debugging code commented out.

...

...

...