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.

matitac now fails if it tries to insert a new alias

new organization of the Base and LambdaDelta modules

Generation of inductive and inversion principles for mutual
inductive types (before only single types were allowed).

Bug fixing. If the inductive types do not occur in t, t is
strictly positive.

moving files

rebuilt

LambdaDelta.ma and some slices of it that typecheck ok!

new problem:
generation of LambdaDelta.ma fails because of complex Cases costructions

Base.ma now ok!!

- semantics of tactic subst allmost fixed
- new tactical progress implemented (not working yet :( )

fixing the semantics of subst

a bit of improvement

aliases removed

added a preamble file with disambiguation information

- new tactic subst removes simple non recursive equalities from the context
- RELATIONAL updated to use the new tactic

cic/test.ml moved to binaries/utilities

Documentation for let-rec fixed.

test file with some bugs

- bumped year
- up to date FSF address

- Level-1: some problems solved
- legacy: one alias added

- Level-1: some fixes to the extraction procedure
- tactics: subst id now works (preliminary)

- makefile added

- record constructor alpha-converted

- Level-1: added two problems
- legacy: added some aliases
- CicNotationPp: fixed output syntax of records

- Level-1: added some problems
- legacy: some now aliases

- changed baseuri

- removed () around sorts

- added some aliases

changed baseuri

- added problem 2
- changed baseuri
- some fixes

- Unified    : some definitions of unified \lambda\delta
- level-1    : \lambda\delta exported from Coq (not working)
- RELATIONAL : added some notation
- cicNotation: some patches to the parser and pp to make them match

trying to make output notation parsable

some properties of NLE

- new legature == for \equiv used in the notation for NPlus
  FIXME: notation precedence not correct w.r.t. \to \land ...
- added notation for NLE
- added a comment to dependenciesParser.ml :p

new naming

removing old contrib dir

changing the contribution name

new naming

info about where to find LablGtkSourceView now

lablgtksourceview is moving to gna, removing the old stuff available here

...

...