Backporting from new Matita:

Patch to avoid double creation of metavariables changed to a simpler one
that keeps disambiguating twice the term. The old patch introduced a few
bugs that were difficult to fix.

Notation for - (clear).

Big change:
 - new command "include alias" to include only the aliases
 - "include" now always includes the aliases and it includes everything else
   only if the file has not been already included

New syntax -H1 .. Hn for clear

Patch to avoid double creation of metavariables changed to a simpler one
that keeps disambiguating twice the term. The old patch introduced a few
bugs that were difficult to fix.

exp and factorial

some progress

Semantics of try changed (fixed) when applied to multiple goals that can now
fail independently.

Back-portin from new Matita: semantics of ntry changed (fixed?) when applied
to multiple goals.

Back-porting from new Matita: improvement to inferred type.

first commit for Helena 0.8.2
autCrg: we removed the computation of the de Bruijn degree
output: we renamed some reductions to reflect the latest terminology
brgSubstitution: icm related bugfix

It is now possible to pass a ${ident x} to another previously defined
notation that expects an ${ident y}.

[ porting from CerCo's Matita ]
1. new implementation of normalize to have a speed up in case of fully applicative terms
2. all reduction tactics used to end with instatiate that re-checked the conversion using
   unification (!!!); added a new flag ?(refine=true) to instantiate to avoid this expensive
   check when we know it is useless

Bad default for ?dorefine for instantiate

1. new implementation of normalize to have a speed up in case of fully applicative terms
2. all reduction tactics used to end with instatiate that re-checked the conversion using
   unification (!!!); added a new flag ?(refine=false) to instantiate to avoid this expensive
   check when we know it is useless

porting to new syntax

Bug fixed: propagation of left expected parameters is now working correctly also
in case of \ldots.

Bug fixed: propagation of left expected parameters is now working correctly also
in case of \ldots.

In the case type_of constructor with expected type T, T is now put in whd to
find an expected inductive type.

In the case type_of constructor with expected type T, T is now put in whd to
find an expected inductive type.

Back-porting from new Matita:

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

Back-porting from new Matita:

Propagation of left expected parameters in typeof.

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:

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).

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