o-algebra defined again

Categories and subsets compile again, hopefully with better universe levels.

WARNING: partial commit to try to understand something.
I have fixed the universes in categories, adding a new category (of level 2)
and trying to prove that powersets form a SET1.

Failing, so far.

Some more fixes. Boring and stupid!

Some fixes.

O-Basic Topologies do form a category.

A few more lines.

Some notes by Giovanni.

Some notes by Giovanni.

added some virtuals

bug fixed, all convertible was called without a metasenv

Just copied here from formal_topologies.ma.

More (ugly) work.

...

Beginning of o-basic_topologies.

Some clean up.

Concrete Spaces defined but... they require about 20m to type-check!

1 more lemma

one line

some work

ums got rid of

1) no more DAEMONS
2) f, f-, f*, f-* are morphisms now

merged commits, the same proof is missing :-(

bleah

Using the new category SET.
Rewriting is no longer working as expected.

New category SET (whose objects are setoids).

we started the support for naive sort inclusion

better pp of virtuals

...

more pps

type3

ranking hopefully fixed

...

fix exponentiation

go notation go!

fixed, it seems the new handling of hints in some rare cases made inference stupid

...

...

...

added aliases for _ and fixed greek leters thanks to wilmer

better pps

handles bad Appl

added better debug_pps and add_user_provided_unification_hint

...

added unification hint

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