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

include also gdome2/ dir in the ocamldoc include path

* debian/rules
  - add additional flags for ocamldoc using "+=" instead of "=" ...

why the heck configure was committed?

* debian/control
  - port Vcs-Svn field to the new syntax
  - add XS-Vcs-Browser field pointing to HELM's repository browser
* debian/rules
  - enable ocamldoc api reference generation (via CDBS)

init new dummy entry

remove spurious comment

upload to unstable

remove spurious entry

  - s/Source-Version/binary:Version/ substvar

add stdlib/gdome2 to the include dir for ocamldoc

bump version

* convert comments in .mli interface files to ocamldoc comments
* bump debhelper compatibility level and dependency to 5
  - enable generation of ocamldoc api reference (via CDBS)
  - added XS-Vcs-* fields pointing to the svn repository
  - bumped build dependency on ocaml-nox to >= 3.10.0

convert comments to ocamldoc comments

1. fix_arity fixed: the code is totally wrong and this is just a quic&dirty
   fix
2. first real-word example in coercions_russel: a certified "find" procedure
   from the ocaml library

Note: removing the (... : Prop) cast from the example, unification fails badly.
To be understood and fixed somehow (i.e. with an Uncertain in place of a
Failure).

This cast now works!

 (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1])
:
 ∀l:(∃l:list nat. l ≠ []). ∃l1.∃a.a :: l1 = l

when a coercion is passed through a case on right-params-free term m,
branches and outtype are adjusted to receive an extra argument (refl m)
to have extra assumptions on it substituded. see tests/coercions_russell.ma

some simplifications.

ooops, missing )

disabled coercions when refining paramod proofs (attemt to understand the slowdown of night-tests)

fixed propagation under Fix/Lambda/Case of coercions, better names are
generated.

there is still a question for CSC about the context of the metavariables opened
by example 51 that seems too long.

code still needs some refactoring, auxiliary functions are ready to be
lambdalifet out.

potential slowdown: The coerce_atom_to_something now looks for the *best*
coercion, where best means the one that opens the least number of metas.

Some simplifications.

coercions under Fix and Case. Code refactoring needed

added a duplicated implementation of replace lifting

...

- lybrarySync:
  patched generation of published xml files: inner_sorts were not considered
- natitaInit:
  patched configuration parsing priority

- matitaInit matitaprover matitadep matitamake:
  fixed configuration precedence:
  cmdline > configuration_file > default
- core_natation:
  added notation for single step parallel reduction: =>
- LAMBDA-TYPES: some new theorems
- LOGIC: some new definitions

added fix case

coercions are propagated under Fix (but not mutually recursive Fixes)

Dandling ")" removed from notation for 'exists.

Composition of coercions with arity > 0 is now implemented correctly.

A test for propagation of coercions (that open new goals) under lambdas,
cases, etc.

1. composition of coercions with saturations > 0 is now implemented
2. as a side effect, there is no longer any difference between composition
   of coercions and the compose tactic

TODO: composition of coercions having arity > 0 is not implemented yet

alpha conversion to avoid case-insensitivity of MySql on my laptop.
OK, I know, I should fix it...

baseuri changed

fixed coercions between arrows when the arrow is dependent.

captured exception preserved (was replaced blindly with a RefineFailure)

reverted assertion, since it may happen to look for a coercion to funclass
even outside fix_arity (in cicRefine/eat_prods)

refactoring of all coercions code and add a check to not perform a coercion check if it is not needed

bugfix in computation of src and tgt for coercions with arity > 0

tests for coercions under lambdas

Coercions are now generalized to the general form
f: \forall xs:Ts. \forall a:A xs. \forall ys:Ts'. B xs a ys
where f is declared as a coercion from A ? to B ? ? ? using the syntax

   coercion uri arity saturations

where:
 1. arity and saturations are optional with default 0
 2. the saturations option is the number of ys

Useful example: it is now possible to declare a coercion from
 nat to \exists n:nat. 0 \leq n
obtaining something extremely close to Russel (the new implementation of
the Program tactic of Coq) up to the fact that coercions are not propagated
yet under mutcases and fixes.

TODO: composition of coercions having saturations <> 0 is not implemented
yet (but should be easy to do, at least on paper)

Coercions rework:
- new functions:
  - coerce_to_sort
  - coerce_to_something
  - coerce_atom_to_something
- added call in Cast
- coerce_to_something goes under lambdas in both
  variant and contravarian positions, to if there are
  c1: B -> B1 and c2:A1 -> C coercions, you can cast a function
  f: A -> B to A1 -> B1.

coercions from funclass are not supported

...

bla bla bla fallback

added a binch of svn:ignore

add a fallback in case the binaries are in the path and not in the runtime base dir

print few more wired assertions

the version on the livecd

more stuff to reach an intensional definition of finite sets

added an utility function

0.2.0

* definition of implication free propositional formulas
* definition of a classical semantics
* proofs of correctness of some syntactical manipulations to reach
  normal forms
* definition of sequent calculus trees
* proof of soundness of sequent calculus derivations
* proof of completeness of sequent calculus derivations (unfinished)

A primer for Matita with some easy, medium, difficult and impossible exercises.

We define proof tree tracks and normal proof tree tracks separately

refactoring

proof by "introduction" (impi) implemented in full

thread-based interface activated again

Bug fixed: RewriteLR were not recognized correctly. Moreover they were also
handled incorrectly (according to the is_top_down flag that should be irrelevant).

Bug fixed: the initial metasenv used in the two tactic was empty!

Avoid reusing Hbeta several times.

select now works correctly even if multiple hypotheses with the same name are
present in the context.

Avoid confusion for names of proofs put in the applicative context.

"obtain H E1=E2 by proof" is now working

little change to theorem eq_gcd_times_times_eqv_times_gcd

removed generic_sigma_p since generic_iter_p is the same

something was really too slow...

default equality stuff filtered out from hint rewrite

removed comments in proof presentation

renamed generic_sigma_p.ma to generic_iter_p.ma

added 'rewrite' option to the the hint macro. a cicBrowser with all library
objects that may rewrite the goal is displayed.

We add a binary for computing the "heights" of helm objects
[this is related to the height of the dependece tree]

added development path normalization, inclusions with '../' in the path should now be handled correclty

auto -> autobatch