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

Missing alias added.

Preamble is now working properly and it does not include unwanted aliases.

error in preamble.ma

subst0 completed

some theorems about getl

Bugs fixed:
 1. matitamake now correctly creates dependencies of the form "A/f.mo: ..." (it used to create
    useless dependencies of the form "/T/A/f.mo: ...")
 2. matitamake is now more (indeed too much) verbose when matitadep fails

matitadep used to raise Not_found on empty files and in some other occasions.
Fixed.

removing unnecessary file

dependences fixed

plist added

removing working file

new theorems

fixed coercions. composite can't occur if to funclass

fixed includes

other working theorems + iso_trans axiomatized (proof saved in problems)

BIG FAT COMMIT REGARDING COERCIONS:
- multiple coercions from the same type
- coercions to funclass
- fixed cicPp for letin and pi
- improved coercions ma with a minimal test for funclass
- cheanged XML and Ast to support `Coercion ARITY label
- added syntax:
  coercion URI ARITY
  recordfield :ARITY> type
- added topological sorting module (funcotr) in extlib
- abstracted graphviz to allow non strict and tred graphs
- tentative (not yet properly done) of hiding coercions in content
- fixed a problem in metadata contraints iof there are no constraints
- renamed/moved/commented some functions (eat_prod related) in the refiner
- crossed fingers

firs error: iso/props

More aliases.

no-indent

removed non XML comment line

the in clause of the match costruction was wrongly output

Aliases are now wrote down even during the first pass.
The only case they are not written down is that of multiple passes.
This makes the scripts more robusts and faster.
We still need (more and more) one shot aliases.