ocaml 3.09 transition

0.7.2 version (ancient)

- more resilient to proof checking failures during pretty printing
- do not compute inner types for sequents

support pretty printing of Cic.Implicit

bugfix: return unshared sequent when applying cic -> mathml transformations so that paste work again

Debugging code commented out.

Error messages improved.

"Localization" of error messages for eat_prods and applications.

Less verbose error messages.

Last details.

Proof using function induction terminated. It's really gorgeous.

Lost of redundant typing hints removed from the functional induction term.

New proof based on an hand-made functional induction.

Useful lemma added.

Invariant no longer true (since when?)

More informative error messages.

split body away to ease inclusion from elsewhere

split to easy inclusion

typo

internal quantification fixed

fixed URI regexp so that URIs containing '-' are allowed

"let rec f = ... in f l" used to be compiled incorrectly
(without checking if f occurs in l and without delifting l!!!)

theorems about equality in classes

some definitions about subsets

Error messages improvement.

Less verbose error messages (= substitution applied everywhere, terms pretty
printed in their context) are now printed by default.
There is a flag in cicUnification.ml to set the error messages to the
verbose mode.

Wrong reported error message fixed.

More information is now printed when reporting errors.

Typo fixed.

Disambiguation errors are no longer thrown away. They are now collected
and presented (in a not understandable way) to the user.

some renaming

Coercions are now inserted also around the sources of lambda abstractions.

more work for coercions

fix

fixed coercions undo

added debug items for enabling/disabling pretty printing notation completely

added support for enabling/disabling (pretty printing) notation

fix for coercions

Incredible bug fixed: coercions were computed and then partially thrown away
during eat_prods!

some more on tinycals

added more on tinycals

Improvement/bug fix: rewriting in the hypothesis used to simplify the
new hypothesis. This is no longer done.

...

New test for parallel rewriting in the hypotheses and in the conclusion.

Comments changed/removed.

"Parallel" rewriting in a list of hypothesis and in the conclusion is now
allowed.

Major code semplification and improvement:
 1. the proof term generated used to have a (Hletin) ...
    Now it has a (H) ...
 2. the code has been greatly simplified by renaming the old variable
    first and doing a letin later; I used to do the letin first and
    rename the new variable at the end

aded a prototype of chtting aboit tacticals

filled disambiguation algorithm section

First draft implementation of rewriting in an hypothesis.
Highly incomplete. Fails randomly if the pattern is not one the tactic is able
to cope with.

New tactic rename (for now for internal usage only).

matita.tex

followed kluwer guidelines

Inizio stesura parte su "libreria tutta visibile".

ported to kluwer style

fixed some stuff in the patterns section

fixed some stuff in pattern section

tests and tests.opt targets greately simplified

added first draft for patterns

predicative subsets started

snapshot

- begin{grafite} environment for script snippets
- more on disambiguation phase

dump_moo.opt

do_test.sh no longer prints the compiler options (used to avoid awk-ing out
the -noprofile flag)

New framework for regression of bad tests.
Now do_test.sh should always return OK if everything is "correct"
(i.e. if good tests are OK and bad tests FAIL with the expected output)

universal quantifier added

The .depend must not be committed! Fixed.

ignore bibtex litter

1. handling of tests and tests.opt targets improved
2. new target cleantests.opt
3. new directory bad_tests with tests that should fail.
   For each test that fails we check if it fails with the expected error
   message.

TODO: the nighlty benchmark could fail to detect the output provided by
the failing tests in the bad_tests directory.

added content level ref

- draft of the first part of disambiguation subsection
- use bibtex

New directory for bad tests with checks on the error message.

...

Debugging code commented out.

Bug fixed: wrong exception was raised (instead of returning false)
when eq_carr-comparing two different things

cic concrete syntax (w/o notation)

better output formatting

removed grammar rule which used to enable things linke "theorem a."

list_uniq abstracted on equality

fixed self and removed more DUMMY... only one left

added print_grammar

removed duplicate entry

tex macros, checked in disambiguation section from whelp paper

dded missing catch for coercions

contribs/PREDICATIVE-TOPOLOGY added as test directory

bugfix, use database name

Introduction, again.:

first draft of db filling script

Introduction (partial).

Introduction.

added an example of reduction of R' and some comments (plus a fix in the demonstration)

Definition of system T.

paper skeleton

Several changes.

A couple more of references.

typos

added Makefile, llncs style, cvsignore

Headings of the matita paper.

Extended bibliography.

Added an example (well founded recursion).