fixed metaconvertibility that was completely wrong.
is_identity and is_weak_identity fixed accordingly

removed bad guard that was always false (assert false in the line above)

fixed (dasabled paramod)

renamed inference in founif that is more appropriate

is_identity -> is_weak_identity

hack to make the Pp work (sometimes)

new version of auto that is able to prove the irrationality of sqrt(2)

added tests for auto

restored the good factorization file

ported to the new reflexivity implementation

maittaprover uses another format

...

removed a useless printing

added metas local context maction: ?n[...]

solved issues regarding SQL incredible error proness

Implemented topological sorting according to the dependencies.

auto snapshot

...

More work on the translation of technicalities/setoids.ma.

One less open helps understanding the code!

More informative error message.

fixed bug regarding developments. paths given with -I are now made absolute

New bug found in disambiguation of records.
To fix the bug it is necessary to propagate the substitution computed
during the type-checking of the constructors to the types of the inductive
types. This is quite complex to do. One possibility is simply to add the
substitution to the proof status.

Initial work on setoids:
 - AST changed to make it more parametric on terms (for the Relation command)
 - functions that work on ASTs consider the constructors in alphabetical order
 - initial translation from Coq to Matita of library/technicalities/setoids.ma

Initial work on setoids:
 - AST changed to make it more parametric on terms (for the Relation command)
 - functions that work on ASTs consider the constructors in alphabetical order
 -

Added generation of dependency graph for the ocaml modules in matita/
WARNING (and happyness ...): first Ruby script added to our repository

rebuilt

Two tests used to have the same baseuri. Very bad.

added SRC parameter to makefile (the one placed in the root of a development) to specify the set of files to handle (if omitted all files reachable from the root dir of the development are used).

The precedence level is now an optional argument of the content to pres
transformation for terms.

linkonly now also links matitac

* ocaml => components
* initialization was missing

discriminate => destruct

{discriminate,injection} => destruct

injection_tac and discriminate_tac now replaced by destruct_tac

injection_tac and discriminate_tac now replaced by destruct_tac that
performs either injection or discrimination. In Coq destruct is called
"analyze equality".

Several bugs fixed in discriminate.
Discriminate now works on inductive types with any number of left or right
parameters.

Bug fixed: a number alias Num 0 now subsumes the case Num n for each n.

last fix.

using lua5.1 instead of lua50

override USER with bench

added $(USER) so that the night bench can override it (and not put garbage in MY sql tables)

fixed script to make csc happy

Bug fixed: aliases for numbers were no longer handled correctly (since 0 was
a wildcard only for symbols).

auto snapshot

snapshot of queries for auto+paramod

added notation

...

apply now uses both menv and subst to decide the fresh meta number

"21" -> "Implicit found"

added displaying of the dep graph of a development, click action still missing

added generation of the .dot version of development dependencies

Injection now clears all intermediate results introduced.
Injection code reindented.
Baseuri in injection.ma fixed.

1. bug fixed: injection now performs recursion lifting correctly
2. bug introduced: injections now behaves as id_tac when it has nothing to do

Added new target linkonly to link matita without re-compiling anything.
Useful for rapid debugging in bytecode.

last problem elegantly resolved!

removed old .cvsignore files
ready for 3.09.3 and ocaml.mk

ready for 3.09.3 and ocaml.mk

binNMU safe setting of debian/*
ready for 3.09.3 and ocaml.mk

Yet another refinement error localized.
Enrico should really learn to localize his own exceptions :-)

Debugging code deactivated.

useless files removed

exportation completed!!

removed useless file in source package

new release, binNMU safe

ok up to pc1

1. Stricter controls implemented in injection.
2. tests/injection.ma now contains a description of why the tactic sometimes
   fail and there is nothing really cute we can do with it. It also hints to
   an alternative solution implemented in Coq.

Bug fixed in injection: lifting was not performed correctly, but it worked
most of the time :-)

1. added a test for injection
2. injection now works also on inductive types with left parameters

As the test shows, there are still bugs even in the case of an inductive
case with right parameters only.

Bug fixed in pretty printing in new syntax of MutCases on inductive types
with left parameters.

Bug fixed in injection: injection can now work on inductive types that have
right parameters. It is still bugged on inductive types with left parameters.

ok up to pr3

removed contribs from nigtly bench

some fixes to the "test notturni"

problems-4 was due to trans_eq expecting an explicit named substitution.

- ok pr0 pr1 pr2
- added one problem (like problems-4)

1. Some warnings about unused warning fixed (hopefully well)
2. We now try to print the MutCase in the new syntax.
   This fails silently when the type of the constructor is not a spine of Prods
   ended by something not convertible to another Prod. It also fails providing
   reasonable information when one pattern has not enough Lambdas.

Bug fixed in injection: a missing lift bugged the tactic when the constructor
had more than one argument.
The tactic is still bugged when the inductive type has either right or left
parameters!

Possible bug fixed (similar to the previous one, but in another similar function).

Bug fixed in the guarded_by_descructors function: in some cases the context
was missing the left arguments! This is the first bug found in the kernel
after quite a long time.

Bug fixed in the guarded_by_descructors function: in some cases the context
was missing the left arguments! This is the first bug found in the kernel
after quite a long time.

Foo is the problematic elimination principle.

ready for the upload

added me as an author, better formatting of debian/copyright

rebuilt

committed the generated version of configure, so that it gets exported upon svn-buildpackage --svn-export

use autotools class so that configure is invoked by cdbs

bumped version

snapshot: first draft of binNMU safe cdbs packaging

added detection of native code compilation in "upstream" configure/Makefile (going to remove it from debian/rules now ...)

oops: changes should be committed to Makefile.in, not to Makefile

ok up to arity assignment

one problem still remains

3 problems solved patching the alpha-conversion of coq 7.3.1

Bug fixed: "by ... we proved ... that is equivalent to ...": the is equivalent
to part was not considered because of a stupid typo.

contentPp.ml (dead code) removed

Dead code (that produces an ugly rendering) removed.

removing unnecessary files

- some theorems from levels_defs
- a new problem

ok up to tau0