Back-porting from new Matita:

- GREAT: when unifying ?1 : Type[i]  with ?2: Type[j] the unifier
  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.

Back-porting from new Matita:

Bug fixed: analysing inductive type that contains implicit used to
duplicate the metas in the metasenv since the term was disambiguated
twice, in the analyze and in the tactic that uses the analyze.

Propagation of left expected parameters in typeof.

- GREAT: when unifying ?1 : Type[i]  with ?2: Type[j] the unifier
  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.

New behaviour of fo_unif: in case of  ?f args == t args'
where at least one args is flexible, it now unifies in parallel even if the
two args have different lenghts (as in the old version of Matita).

Debugging code commented out.

Debugging code commented out.

Debugging code commented out.

Small improvement: check now takes the context of the first focused
goal, if any.

Some arithmetics.

- lddl html pages: the transition to xhtml 1.1 + css 2 is complete
- helena: we made a 88 x 32 label for the Web

Implementation of proof irrelevance finished.

Debugging disabled

- auto now uses the equality of the new library

- dead code removed

- number notation ported to new library
- code for number notation made less general by hard-coding the only
  notation

Number notation ported to new library.

Invariant dropped: NotationPt.NCic t can now contain metas.
We do not know if the invariant was exploited somewhere...

Bug fixed: analysing inductive type that contains implicit used to
duplicate the metas in the metasenv since the term was disambiguated
twice, in the analyze and in the tactic that uses the analyze.

we updated the css validation icon

we are migrating the static htnl pagest to html 4 to xhtml 1.1 + css

- stock icons restored
- hbugs got rid of definitely

1) matita.glade ported from glade2 to glade3
2) added a workaround (using xmlling) to convert &#x....; chars generated
   by glade3 into unicode symbols to avoid a corresponding lexing bug in
   lablgladecc2 :-(

let and let rec used wrong tokens

Big bug fixed: grafiteDisambiguate.add_aliases_for_objects used to add
aliases to the status, but not to the .ng.

Fixed, but we probably need a better approach where the addition to the
.ng is performed by the single modules, and not in grafiteEngine as it
is now.

Bug fixed: an assert false was raised before giving the first interpretation.

- bug fixed: fullpath used in place of relative path

- bug fixed: circular dependencies are now detected correctly

now implemented in matitaEngine.ml

Huge change!!!

- matitadep & co removed (RIP)
- both matita and matitac can now recursively compile files as needed
- librarian greatly simplified: now it only handles roots

Probably many bugs left.

- better names, interface simplified

- cleanup

- matitacLib merged into matitaEngine

- dead code removed

- useless code removed

dead code removal: the parser used to be able to return LNone when it
parsed and immediately executed a lexicon command

more dead code removal

dead code removed

- recently introduced bug fixed: the new intermediate statuses for
aliases used to already have all the aliases in them

- refreshing of uris in NotationPt.terms implemented

- lexicon merged into ng_disambiguation

- lexiconSync merged into grafiteDisambiguate

Dead code removed (left from a previous commit).

- disk dumping of ex-lexicon commands almost implemented

- disambiguation code moved from matitaEngine to grafiteDisambiguate
- grafiteDisambiguate.db is now opaque

Dependencies re-computed.

Minor code uniformization.

- further simplifications (??) of the status dependencies

..

All methods made explicit.

dependencies between statuses simplified

dependencies between statuses simplified

Minor code clean-up to simplify module dependencies.

- dependencies between statuses simplified

- content/interpretations.ml and ng_cic_content/nTermCicContent.ml where
  mutually recursive and part of the status was kept imperatively;
  the two files have been merged together into ng_cic_content/interpretations.ml

- some changes in the crux icon
- the installation of the icons is now automatized

- dandling code (to be put somewhere) implementing recursive compilation

- interpretations are now saved in the .ng files

- Print/Set commands removed
- stupid bug fixed in interpretations: we did not add the new id to the
  id list, so that only the first interpretation was considered
- added a new field to the interpretations status to record the recently
  added aliases that need to be made explicit in the script; much better
  than what we did before (alias diffing)

last commit for helena 0.8.1

- xsl      : we can render the levels of the abstractions
- ccs      : we output three kinds of constraints
- Makefiles: we automatized the relising process
- brgCrg   : all abstractions have infinite level for now

notation kind of works

- LexiconAst merged into GrafiteAst
- all lexicon stuff made functional (more or less)
- no more .lexicon files

- the connections between the intermediate language and the "bag"
kernel were missing
- the connections between the intermediate language and the "bag"
kernel are now tail recursive
- the dtd now declares the "level" attribute
- some "assert false" removed in crg
- xml exportation of the data processed by the "bag" kernel is now
available
- the "bag" kernel now uses Entity names rather than identifiers

big change in parsing, trying to make all functional

- some bugfix
- some
- old intermediate language (meta) has been removed

the old intermediate language (meta) is now obsolete

when sort inclusion is enabled, we can produce conversion constraints in xml
format

a module was missing .........

- initial support for abstractions with explicit levels
- some minor bug fixes

More parts of the lexicon status made functional.
Still mostly untested.

Porting to new syntax.

Porting to new syntax.

Porting to new syntax.

Porting to intermediate syntax.

Bug fixed: a missing eta-expansion raised an assert false

WARNING: partial commit.

- matita is compiling again, but totally untested
- major re-organization of the statuses

WARNING: partial commit (does not compile)

1) major re-organization of statuses
2) major change to dumpability
3) partial functionalization of lexicon status

- grammar of // changed to move the justification inside;
  reason: that brain damaged piece of software that is CAMLP5 does a
    lookahead and then it forgets to rollback the token (why??? is it
    a bug). As a consequence matita used to work (since it parses a
    statement at a time), but not matitac (since the lookahead destroyed
    the next command)
- core_notation.moo: \frac used to be at level 90, but this is incorrect
    during parsing and incompatible with the new syntax; \frac is now
    used only in output
- minor dead code removal here and there

Dead code for .moo files removed.

.moo no longer used: all interesting data is left in either .lexicon or
.ng

Bug fixed: heuristic to detect real URIs used to raise an exception.

old standard library no longer included

add some virtuals

urimanager removed

fix queries

Last commit made matita FTBFS. Fixed.

Some files ported to intermediate syntax to test.

STATS removed (was it still working properly??)

cic module removed (RIP)

tentative parser patch with symbolic tactics names

elim implemented as a notation for apply

Bug fixed: it always made an undo to the empty status (stupid bug
introduced in last commit)

camlp5 probably changed some internal data structures and now they cannot be compared with pervasives.comapre, thus we avoid it. Was breaking the natural deduction stuff

fixed many scripts that broke for various reasons

backport of patches to unification

fixed List.for_all2 called without knowing if the two lists have the same length

new case for higher order unification:

  (? ?) =?= (f x)

is not handled by delift, since flexible arguments in the local context
are skipped by delift, resulting in the instantiation of the head meta to
a constant function, even if the rhs is structurally the same.

removed wrong optimization in delift and export is_flexible

the Makefile was still calling transcript.

transcript removed (currently useless)