Path fixed.

Code extraction branched.

Temporary stuff to test code extraction. Running make produces
extraction.hs which is checked by "ghci extraction.hs"

1. Implemented type inference for Fomega to extract term application correctly.
2. Fixed the Decl classification.

Bugs fixed:
1. the context was processed in reverse order
2. the classification of types was wrong

Bugs related to pretty printing of names fixed (capitalization, name
clashes, etc.). In particular removed binders (propositionals) were sometimes
still counted.

Tests for code extraction; to be moved elsewhere.

Bug fixed: Haskell forces capitalisation.
But still open: name clashes due to capitalisation.

Begin of porting of code extraction to the new Matita.
The file does not belong to the kernel: it will be moved away soon.
The extraction code is not branched yet and it does not need to be compiled.

work in progress

Termination!

Wip

work in progress

update in basic_2

- context free computation for terms and local environments

additions and corrections to basic_2

- support for pointwise extensions of a term relation started ...
- we now support abstract liftable relations

work in progress

work in progress

polarized binders introduced in basic_2

- matita: reset_font_size () added after matita.conf.xml is read to set
the font size specified by the user
- lambda_delta: equivalence between normal forms irreducible terms
proved (context-sensitive version)

one file was missing ...

- lambda_delta: we updated some notation
                we are switching from context-free to context-sensitive reducible terms
- basics/star:  star constructor refl renamed to srefl to avoid name clash with id constructor refl

- we polarized binders to control zeta reduction
- confluence and strong normalization proved

An executable version of the tutorial.

progress in termination of marks.ma

One less warning.

Some debugging times exposed.

Major speed up improvement after every tactic application.
Exponential algorithm (in the size of the sequent) turned into linear.
It only shows for very large sequents though.

Few changes

- intermediate commit to allow debugging of auto tactic in xprs.ma
- extended computation is now defined (its De Vrijer's reduction rt)
- stratified native validity is now defined (it's supposed to be
easier to deal with than native type assignment)

adding tutorial

porting to termination

- we added a time specification in the generated web pages
- update in basic_2

more symbols added for lambda_delta

- dynamic type assignment dismissed for now
- stratified static type assignment and unwind defined

commit by user mkmluser

commit by user mkmluser

commit by user mkmluser

manual commit

bug fixes

reverted to previous version (plus anchors)

added tick.png

Added NotationPt.name_of_obj.

Cosmetic changes.

Bug fixing + cosmetic changes

manual commit after active hyperlinks

manual

commit by user utente

Matitaweb: several improvements in the UI.

Matitaweb: opening a file resets the status.

Bug fixed: arguments of a match are (no longer...) in whd; so a function
that expects a term in whd was calling herself recursively on a term not
in whd.

New spec. for advance_both_marks

working on termination

removed a duplicate

Closed all axioms in turing (but not universal).
Revised semantics of basic machines for termination
purposes

Hyperlink support.

an addition to basic_2

- star.ma: constructor inj of star conflicts with previous constructor
inj of TC. constructor inj of star renamed to sstep and constructor
injl of starl renamed to sstepl
- lambda_delta: bug fix in reduction rule tpr_zeta which now has the
structure of like tpr_delta. More lemas towards subject reduction of
native typing

adv_to_mark_l

closing a few axioms

additions to basic_2

- relation between native type and atomic arity proced
- higher order native typing defined
- some minor results towards subject reduction for native typing

middot notation

adding match_machines and removing trans_to_tuples

several changes

Reindented

New nohyps option for /demod/

New flags for demod:
  1) by ... now can be used to explicitly give the set of equations to use
  2) nohyps can now be used to avoid using the hypotheses

move_char.ma
-This line, and those below, will be ignored--

A    turing/move_char.ma

merging of char_move_c and char_move_l

A recompiling version

Dropping a coercion and some hints due to conflicts with CerCo

Modifications and refactoring

Msg reporting via HLogger in the error window made asynchronous => speedup.

Patch to avoid generating _inv_ind_recTX for X the largest universe.
Rational: for some unknown reason, that takes ages to fail.

Sys.Break no longer catched

New debugging switch in the interface.

More conjectures proved.

new version of move_char_l suign swap

swap machine; move_char revisited

restructuring

Restructuring

Some results on relations. Moved things around.

Completed all proofs in if_machine

an addition to basic_2

- lambda_delta: subject reduction for nativa type assignment begins ...
                dependecnes between source files improved
- matitadep: little application for optimizing dependences between .ma files
             (used by lambda_delta Makefile)

semantics of the if-machine.
Moved some lemmas to their proper places.

notation

comments

additions to basic_2

- predefined_virtuals: an addition
- lambda_delta: lenv ref for native type assignment completed
                levn ref for substitution correctly oriented

Finalized copy sub-machine of the universal turing machine. Some new results
on lists.

Ci siamo quasi

update in basic_2

- predefined_virtuals: some additions
- lambda_delta: first results on lenv. ref. for native typing
                some notational changes

Thanks to Guarrigue, code for Serializer functor simplified using
private types. The type system of OCaml is more and more misterious...

Progress.

update in basic_2

- nDestructTac: Sys.break handled in two places
- lambda_delta: a major property of native type assignment
                some properties of context sensitive equivalence
some notational changes
some annotations