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

Some notation added

more stuff about coercions

little bug in coercion generation found. it use to create more coercions that expected (luckily convertible).

makefiles updated

makefile updated

matitac: We do not generate the .moo and .lexicon of a dumped .mma
Base-2 : makefile patched

added some notation

added another example in which our coercions are powerful

used ;try assumption instead of .try assumption

; and not . after auto-paramodulation

reverted previous fix

restored compaction of metas at the end of given_clause

Makefile missing in previous commit

New developement LOGIC about the cut elimination of implication for Sambin's basic logic; one of the rules must be corrected (work is in progress)

added test about dependent coercions