Ooops. In previous commit I forgot to subtract the left arguments in case
analysis.

Bug fixed: case analysis where a case had not the expected number of arguments
was not detected.

Bug fixed: a MutCase considering a wrong number of cases was not detected.

Bug fixed: a MutCase with missing or exceeding cases was not detected!

1. More localization: interpretation errors are now loosely localized.
2. Interpretation of pattern matching highly improved:
   a) missing branches are now detected
   b) additional branches are now detected
   c) permutated branches are handled correctly

   Still to do:
   d) check that every constructor is given as parameters exactly the
      number of expected arguments

Recently introduced bug fixed: error localization was not working properly for
the error "more arguments than expected".

bug fix in injection: we have to recur on the generated premises

we revisited the implementation of the destruct tactic in the perspective of joining the subst tactic to it

Debugging code improved.

- new function for general relocation of local references (rels) in terms
- swapped names injection and injection1

fixed copyright file... an ITP should be done

Interesting. Do we need many more inversion lemmas? (Or a different and
dumbier inversion tactic?).

fixed make opt

DOS-style CR+LF added to the blanks list.

Dead code clean-up.

The behaviour of autobatch paramodulation has changed.
But autobatch works! Is the test still correct?

natural number => Coq natural number
The behaviour of paramodulation has changed.

natural number => Coq natural number
The behaviour of demodulate has changed.

natural number => Coq natural number

Wrong test patched.

natural number => Coq natural number

discriminate.ma => destruct.ma

Spurious code removed.
Destruct fails recursively.

natural number => Coq natural number

Old wrong code to avoid old bug fixed.
Error in automation.

Stupid bug fixed.

auto ==> autobatch
Two kind of failures still there:
 1) fails to find a proof
 2) finds a proof, but the proof does not type-check

Stupid bug fixed (I deleted "assumption a" by error).

auto => autobatch

auto => autobatch

Caseness problems fixed.

Some lemmas moves to the file they belong to.
Broken references to renamed errors fixed.

Theorem sigma_p_knm changed into generic_iter_p_knm.
2 specific versions in nat/iteration2.ma and Z/sigma_p.ma

- some new auxiliary lemmas
- some improved proofs

removed unused notation =>

Move to OCaml 3.10. Requires debian packages from unstable (soon in testing).

Fixed baseuri

Part1a update...

More restructuring in moebius.ma

Reorganization of the library.

Reorganization of the library.

Reorganization of results.

Old inversion bug fixed: it used to work only on the last hypothesis (or sort
of).

added patch to allow i,j,k: skip and *: skip

Some axioms for Q.

 added some notation

started the Proof Weight predicate for cut elimination and confluence

bug fix in Track definition
started PRed: parallel reduction simulating cut elimination

Last version of poplmark 1a, featuring new proof, only 558 lines!

we chmod the created directories to override the umask settings

fixed some file permissions (anybody can rebuild a published devel)

- system flag now forks for matitadep too
= legacy Base-1 and LambdaDelta-1 reinserted on tests.
  will compile in system space because they are published

* add Homepage debian/control field

bug fix in configuration dependences

now the -bench and -system flags work for matitamake

Further simplifications to the main theorem about Euler's totient function.

* Some simplifications to theorem in file totient1.ma.
* Some theorems moved from file gcd_propreties1.ma to file gcd.ma.
* Some theorems moved from file dirichlet_product.ma to files div_and_mod.ma and primes.ma.

commented out pack coercion, since the code is not meaningfull.
it was conceived when coercions were toys, now it is much more complicated

some theorems have been moved to more appropriate files in library.

temporary changes, before the complete cancellation of the file.

simplified version of a theorem.

Some new lemmas.

A new function.

unreleased

* debian/liblablgtkmathview-ocaml-dev.install.in
  - more flexible pattern to install ocaml object files, so that missing
    *.cmxa files on non-native arch do not trigger failure with latest
    debhelper

utf8 changed to UTF-8 for compatibility with IExplorer

Qualche semplificazione.

since compat <> 3 no cmx* in the install.in bu just cm*

this preamble was completely wrong :)

a working example :)

the published devels must be removed from the tests

new matita.conf with getter entry to see the published matita contribs and with a db entry to see the public db.
a db sipset for publishing the matita developments is also provided

added a debug print

rdfly patched to work with the new db structure

Updated, proofs are now about 750 lines.

librarySync - we do not generate the object attributes when we publish the xml
LambdaDelta-1 - new cast type rule

some theorem names changed.

replaced an assert false that cause nat_ind not to be displayed with a dummy result

last version with caml 3.09 built and saved as 0.3.0

...

other simplifications.

This test shows one of the few cases were Matita is able to infer a dependent
type. It should break if the dependent type is no longer inferred.

* debian/control
  - add XS-Vcs-* fields pointing to HELM's repository and browser

...

in the case of coerce_to_sort the whd was done with delta:true, that caused an incredible slowdown in dama/
more debug printings added and some comments for vim folding mechanism

other simplifications.

* NOT RELEASED YET

* change how the ocamldoc API reference is generated: no longer use upstream
  Makefile, but rather rely on CDBS
* debian/control
  - remove build-dep on texlive stuff and graphviz since now we only ship
    HTML version of the API reference
* debian/docs, debian/doc-base
  - file removed, the latter will be now automatically generated, the former
    would only contain README and CDBS is smart enough to guess it

huge commit regarding coercions to funclass and eat_prods.  before there was a
so broken behaviour that is impossible to describe the changes.

now:
  eat_prods he hety args

  starts checking if hety is metaclosed, if it is does nothing, if not
  unifies it with ?->?-> ... ->? s.t. there is a Pi for every args.
  if this unification fails, does nothing (all coercions are in the
  second phase.

  continues eating prods in hety and args in parallel, if there is an arg
  and no more prods, tries to fix the arity of (he already_processed_args).
  fix_arity gives a range of possible coercions to funclass s.t.
  (c (he ..)) : FunType. The eat prods and args continues, eting the remaining
  args toghether with FunType. If it fails, it continues with another c to
  another FunType. This recursively (yes, it backtracks. no strong opinion
  here, but there is no sane heuristinc to chose one FunType).

  the code is reduced to 1/3, but Localization of errors probably need fixing.

the order of abstraction is now correct, but there is an orrible hack to make eq_OF_eq have the right type.

removed an assertion that makes no more sense to me

better debug printings

better test for church numerals

just a Pcre expression fixed, nothing real

...

matita can now safely start a matitac that will put metadata in the right db.

Full specification of find. Added notation for If_Then_Else. Probably a delta
on t in the match the decides if it is the case to pass a coercion under a
match whould be nice.

bump version

release

* add ocamldoc comments to .mli interface files