unification hint

lambda case fixed, used to not properly use the expected type if it was not a Prod

added 'unification hint command to add a term to the new unification hint database'

identity coercions are not really inserted, just used as hints for unification

....

Stupid bug fixed: checkin the type in place of the sort during the refinement
of axioms.

New disambiguation commented out.

Many axioms are now proved... using many more (but simpler) axioms.

Now it compiles again.

Refinement of axioms fixed. We did not check that the declared type must be
a type.

- improved logging
- we started to support the coercion for "non"

...

we started the support for the coercions "alle" and "alli"

foo overlap

foo overlap

....

we added the implicit coercion for modus tollens

previous change was causing divergence

hints work better now

hints attached

removed debug code

fixed a bug, it used to report o wrong is_normal bit in case of match

make it compile again

wrap object_not_found

move the printing in the right place

auto expansion of \tex macros added as a switch in the edit menu

added one asser

dep.opt regenerated

added unification hints

Some changes to the pullback test, for debugging

First attempt to implement unification hints.

use named types to force some constraints asap

To check if a term is type, do a whd of its sort before matching it.

...

aded some whd, you should be able to declare something like:
 inductive A : FOO :=
where FOO is defined as a sort (or unfolds to somthing ending with a sort)

The library is no longer automatically used during disambiguation.
It is used only when the user press the More button or when he selects
the library from the Debug (?????) menu!

Moreover, using the library or not using it has now a different behaviour:
1. when the library is NOT used, symbols with no preferences are no
   longer automatically looked for in the library
2. when the library IS used, only passes 5 and 6 are tried.

CONS:
1. the Debug menu voice is now necessary: move it elsewhere? always open the
   disambiguation window making it non-modal? put an hyperlink in the error
   message window?
2. when the library is used, all previous preferences are completely ignored
   for all symbols. This makes the system much more stupid than what it used
   to be.

PROS:
disambiguation is now much faster in case of error

- improved logging
- optimization in subst

new kernel basic_ag (with absolute local references)

we are changing the kernel version from basic_rg to basic_ag

autItem : the uris of the objects involved in the implicit coercions
log     : improved log output
basic_rg: improved logging

...

eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg fd => c ] is
now correctly broken if too long

...

improved type hierarchy management

...

A parser (and a scanner) to import "~C" files into Matita.

...

1. new expressions AND, OR, XOR
2. constants must be initialized
3. bug fixed: the size n of an array means that the array
   has (n+1) elements. Thus the last valid index is n.

- basic_rg: architectural bug fix
- toplevel: more help on command line options

...

added some hardcoded universes, needed to typecheck the librarya

added some messages

added empty_db, usefull to avoid translating all old coercions to obtain a new coercions database

use new function to clear caches so that objects are translated correctly

better error message, functions to clear various caches used during translation of old2new cic, logger functions implemented inside the typechecker so that
uncommenting one line makes the type checker more verbose when recursively typing stuff

thanks to the new fixes to notation, I can define \land for both pairs and
families!

pattern matching over Ast.Case simplified:
- it is not possible to match the `in intype` foo part
- it is not possible to match the outtype
eta expansion still done on Ast (hard to do it in Cic. The abstracted variable
does not have a type :-( thus you may have to double your notations. Name for fresh variables changed to \etaX instead of freshX (much shorter in terms of screen pixels)

Applications are now processed from left to right.

support for mathml mpadded tag added (allows to overlap two subsequent symbols); you library needs to be recompiled after the update

- new semantic log system
- new brg terms
- bug fix im MetaOutput and MetaBrg

first version of kernel "basic_rg"
the grundlagen does not typecheck because some of its lambdas are actually pis
(this is known)

new disambiguatio attached with the right universe graph

raise uncertain when a sort is not a sort but may be, use max for mixing universes, coercions to sort in the prod case are triggered before putting the source type in the context

better coercions indexing and lookup

better max function (instead of @) for combining universes

added an exception

saturate was not returning the correct (saturated) type (but a correct number
of arguments.

fixed notation

...

option to collapse all tex macros implemented

A (boring and long) once-in-a-life exercise on proving a trivial property
on natural numbers in ND.

non active but almost working implementation of \TeX macro substitution while colouring

alt-l for not working nymore for \fox where x was in an eq class

...

better replacement for \\def

3.5 -> 35 to help crappy latex

New exception considered.

Bug fixed: every time we form a Prod, we must typecheck it before trying
unification.

better images

new concept of virtuals, defined only in the gui that behave as the old (still
present and used) ut8tables and ligatures mapping \foo or => to unicode symbols.

support in the gui for utomatical sumstitution of a virtual with its utf8
counterpart (disabled now, grep for if false && str = " ").

support for uf8 equivalnce classes, names simalrsymbols, activated by alt-l.

alt-l is now overloaded, can expand a \foo or => to a unicode symbol
and cycle on unicode symbols in the same eq class of the one just before the
cursor.

classes are already defined for letters mapping them to variants (other
alfabets and fonts) and on arrows and <.

metaAut: now we use hash tables properly (processing time: 2s)
brgReduction: started

new exception captured

Added new syntax  Type[n]  where n is a number.
The old kernel interpretes it simply as Type.
The new kernel as Typen.

Debugging code removed.

Debugging code removed

Debugging instructions removed.

Useless code removed.

Useless code removed.

Useless code removed.

Case-sensitive fixes.

a few missing ~subst added to whd

coercions are there, but not heavily tested

if todo_dom was [] disambiguation was performed twice

still commented, but benchmarks the new/old disambigution process

disambiguation takes ~mk_localization_tbl and not ~localization_tbl, thus can
create the hashtable when needed (after every interpretation)

raise failure instead of uncertain if two terms are meta closed

Fixes:
 - new letin interpretation in nCicDisambiguation fixed to not swap arguments
 - new refiner raises good exception in case a sort in not such
 - reference raise good exception instead of assert false
Improvements:
 - new disambiguation attached
 - constructor -> indty function in reference

housekeeping:
- unused functions removed from Enviconment
- unused file disambiguatePp removed
- disambiguation callbacks pushed down to Disambiguate
  from MultiPassDisambiguator

Bug fixed: pretty-printing of aliases when the OK button is pressed in the
ambiguous error window.

The aliases and multi_aliases in the lexicon status are now
LexiconAst.alias_spec (they used to be DisambiguateTypes.codomain_item).
Benefit: it is now possible to use the very same set of aliases both for the
new and old terms. Moreover, this commits simplifies quite a bit of code.

Known bugs: when clicking the "OK" button in the error message disambiguation
window, an assertion is often raised. When the assertion is not raised, the
set of aliases that are printed are not syntactically/semantically correct.