New version.

New version.

New version.

New version.

New version.

New version.

New version.

First version.

Old algorithm moved to old to leave place to the new one.

cicInspect: node count fixed
proceduralTeX: bug fix
LAMBDA-TYPES/Legacy-2/preamble.ma: bug fix
character: updated

uri renaming and new nodes count

some renaming to comply with new naming policy ...

cicInspect: now we can choose not to count the Cic.Implicit constructors
proceduralTypes, proceduralOptimizer: we do not count the Cic.Implict nodes
proceduralTeX: bug fix

ProceduralTeX completed and tested on the terms given as examples in the paper about the procedural reconstruction

...

...

...

New module for TeX rendering of procedural input/output
Used in the papers about the procedural representation

...

...

- Coq/preamble: missing alias added
- nUri: head comment fixed
- Procedural: the cases tactic is now detected and generated
              but does not compile :))
- grafiteAstPp: output syntax of the cases tactic fixed
- grafiteParser: impovement in the code for the elim tactic

some notational experiments

...

...

...

commented some printings

minor changes to make the library compile after wilmers new exists.

Axiomatization of real numbers (work in progress)

errata corrige.

Fixed a problem of lifting.

some work to refine objs

...

b:action are now considered as m:maction and thus are expanded

...

...

a non necessary but morally required change. The matched term in
are_convertible is compared with test_eq_only=true (not really needed since
if it reduces to something it is a constructor an thus an application that already honors the test_eq_only=true check for arguments

some work to speed up the system

case tactic first tries with a simple outtype and then with a more sofisticated one
only if necessary since refine time may be long

...

CicTypeChecker.typecheck now takes an additional parameter:
- trust:bool, set to false only by the proofChecker daemon, while
  the refiner (for example) passes true

Hmmm, going too low.
We need a more abstract proof (see Theorem 5.15, page 157 old book).

...

Towards fullness.

Renaming.

Renaming.

fix convertibility in case of application test_eq_only is =true for
arguments, since we dont know if reduction eventually moves them in
contravariant position

more polishing

...

application arguments are compared with test_eq_only=true

some work

...

...

...

...

maction, mpadded and mstyle added to documentation

minor fixes

maction support added to notation, adopted for = AKA  = \sub t
deactivated the library/formal_topology directory since it is completely broken and outdated

maction layout added to notation

we were generating a name for the main fix twice

added a number to identical error messages to ease tracing them

OEIS sequence identifier found for P(n)

TODO

some minor fixes

a bit of work done while travelling to padova

- new notation.ma file with local and common notation
- o-bp have now a O as prefix, the same for o-cs
- BP_to_OBP proved to be a functor, not faitfull nor full (simply stated)

...

...

all pullbacks are attempted in sequence, removed many unfold

universe inconsistency fixed

SUBSETS_full up to universe inconsistency

faithful

CAT2

ceommented out metasenv

...

Sambin's result holds trivially since most of the fields of the objects of
the two categories are definitionally equal!

basic topologies are trivially o-basic topologies
the same for their morphisms

1. new coercion(s) from CPropi to CProp
2. fixed notation for subsetS
3. coercions still have problems: the coercion from objs1 REL is not
   accepted because it is identified with the coercion from objs1 SET

the new coercion behaviour (variants + composition with ID) and the new
discipline of declaring hints for carrier of structures (setoids and categories) and no
other hints simplified many passages

added notation for 'Vdash

if the user attempts to insert a duplicate coercions the system forbids it

unvariant also for coercions to funclass

- name mangling changed, added __ to separate additional number
- composing a coercion with an identity does not affect the body, and a variant is generated

no more universe inconsistency printed to stderr

coercions that are marked as variant are unfolded when inserted

Coercions graph is printed between real types and not approximated ones

o_continous_relations are really o_relation_pair... up to a bug of Matita
(a meta left in the metasenv :-(

o-basic_pairs are indeed examples of o-basic_topologies!
some more work is required to prove the same for morphisms

many changes regarding coercions:
- new `prefer coercion foo` command to reorder the list of coercions associated with a src >-> tgt pair
- rewritten coercions undoing mechanism
- coercion composition fixed (generates more coercions)
- librarySync rewritten, procedures to generate derived lemmas (eliminators, invertion lemmas, ...) are hooks registerd by other modules that can thus live anywhere (also in tactics/ like the one for inversion)
- manual fixed to talk about the new command
- coercions graph is drawn together with a list of coercions that makes their precedence visible (and can be altered with the prefer coercion command)
- dump-moo fixed to print coercions
- removed `Coercion attribute in XML files (YOU NEED TO RECOMPILE)

- Added new output in standard C.

Some work on o-algebras towards the proof that a and j are saturation/reduction
operators.

The new coercion from SET to Type0 with higher priority really helps a lot:
almost all explicit occurrences of carr have been removed.

more composites to make all happy!

eq over SET1 and SET no longer used

some more if/fi conversion due to the new . binding

unary_morphism_N : seoidN -> setoidN -> setoidN (was ... -> setoidN+1)
notation for . is now bound to fi instead of if (i.e. rewrites -> )

virtuals for () removed and bound to 'o'
memory changed, used similar symbols are presented first but not altering their original order

Just a snapshot.

coercions reordering implemented

updated

More work on concrete spaces.