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

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

...