Basic pairs restored; require renaming to use them together with o-basic_pairs.

Some progress: everything works well now.

Ooops, I forgot to commit this in the previous 3-4 commits.

An hint moved to the right place.

No more daemons, no more exTs.

Great: some significant progress in fixing universe levels.

removing (only from the interface) functions related to ligatures that now live in the GUI

added help on virtuals and UTF-8 equivalence classes

expand ligatures after \n too

added := -> \def

added some memory to virtuals eq classes

...

1. CProp_n fixed to be equal to Type_n to better understand what is happening
   with universe levels
2. major proof step: I have proved (up to universe inconsistency :-( that
   every RELation induces an OA morphism. In particular, these means:
     A) having correctly defined the four images on subsets
     B) having proved the fundamental symmetry
     C) having proved the two fundamental adjunctions

Snapshot to try to understand something.

Some more progress, fighting universe inconsistencies.

Yet another universe problem :-(

...

Back to step 1: all files that used to pass now pass again.

More re-organization.

Basic pairs went through with no problems.

Universe level fixed (litterally).

Niceness was just a temporary illusion :-(

Much, much nicer now.

Some more re-organization.

More re-working.

More reorganization.

equivalence_relations made uniform w.r.t. universe level
However, there is still a bug related to universes, which I do not understand.

Final work for today.

removed duplicate notation

Some more painful work.

binary_meet is back again, with some effort

Many universe inconsistency avoided here and there.

The universe inconsistency comes from big union, that uses the existential.

Proof that \Omega \sup A is an overlap algebra, up to universe inconsistency :-(

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