ported to the new destruct

Arguments of constructors in a case pattern are now ppid-ed.

svn:ignore set

please, commit files with debug=false otherwise the distributed matita prints a ton of dust

forced associativity in if construct

Zoli's note (in Italian) about a constructive version of Lebesgue's dominated
convergence theorem in a point-free setting.

set svn:ignore to *.ml in the deve directories

- bug fix in destruct
- old subst tactic removed
- some tests fixed

reorganization of the whole story, the root dir contains the algebraic structure

Code extraction unbranched again.

new implementation of the destruct tactic,
which includes the old subst tactic (now removed)

cic_acic should be compiled before cic_exportation

Bug in detection of too polymorphic types partially fixed (see comment).

MutCases that occur in types should be handled with "any type".
Unfortunately, such type does not exists in OCaml. For now I generate
unit with a comment. Applications to arguments will fail and require another
Obj.magic.

Obj.magic are now generated to extract dependently typed MutCases.

Handling of left parameters of constructors/indutive type definitions improved.
Bug fixed: arguments of sort Prop were not dropped from MutCase branches.

Slightly nicer output.

Filenames are now fully mangled (e.g. matita_nat_nat.ml) to avoid file name
clashes.

Type application and abstractions are now exported correctly.

New OCaml keyword "val".

"f" => "aux" to avoid name clashes

The type parameters in an inductive type declaration should be the left ones,
that are replicated in every constructor. They used to be listed n times for
an inductive type with n constructors.

Type arguments are better uncapitalized.

Empty types not in Prop and empty types elimination handled correctly.

Empty and singleton type elimination are now handled properly.

1. type definitions of propositions are no longer exported even if parametric
2. arguments of type definitions are now printed correctly according to
   OCaml awful syntax

Bug fixed: qualified names were not generated correctly when the dirname was not
empty.

* type definitions that define a new proposition are no longer exported
* type arguments of type Prop are no longer abstracted in inductive types

CicExportation branched. Change "if false" with "if true" to activate automatic
exportation of OCaml files during compilation.

All exported names are now qualified. This avoids the need for "open" statements.

All names are now qualified. This avoids the need for "open" statements.

*** Very experimental and not branched ***

Exportation to OCaml partially implement in cic_exportation.

It can already export several files from the freescale development (also not
committed yet).

Still to be implemented:

 a) erasure of term dependencies from types
 b) extraction of "open" statements
    [ I do not know how to implement this! ]
 c) extraction from CurrentProof
 d) extraction from Let-In
 e) extraction from CoFix
 f) extraction from mutually recursive inductive types and Fix

Known bugs/missing features:

 1) All the "classical" ones (described, for instance, in Letouzey's papers).
    In particular, terms may diverge, singleton elimination and false
    elimination not implemented in the correct way, Obj.magic not generated
    where needed, etc.

 2) Name clashes can be generated by the extraction. OCaml keywords may be
    chosen. And so on.

- tacticals: new tactical ifs added: uses thens where if_ uses then_
- ProofEngineHelpers: namer_of exported from GrafiteEngine

Added an hook useful in many situations.

finisced configuration section

added doc for db and getter sections

added notes about sqlite and removed obsolete zack repository

New image from Tassi's PhD thesis.

better implementation of if_

remade dependencies that were wrong

- destruct: core of subst tactic implemented,
  must be linked to destruct in order to work
- "if" tactical implemented (used by core subst tactic) - to be tested
- added freqently used constant hole = Cic.Implicit (Some 'Hole)

 reverted matita db configuration fixed

Bug fixed: patterns in hypotheses under binders where not computed correctly
because of a bad and wrong hack. Replaced with a correct solution. However, a
better unimplemented one exists (see new comment).

Note: copy&paste as multiple pattern not implemented yet. But it seems very
easy to do.

New syntax for match patterns in terms and in patterns.

The document was not valid. Fixed.

Pretty-printing of "match ... with" pattern syntax fixed. We need an
~output_type flag since the semantics of patterns is slightly different from
the semantics of terms (and maybe this was a very bad choice I made):

match p return p with [ _ => p | ... | _ => p ]

Nil => nil, Cons => cons

Nil => nil; Cons => cons

New syntax for match patterns.
New semantics for destruct.

clean can't fail

added patch for the configuration file

reverted last commit

...

rebuilt

no -rectype passed to ocamldep

rebuilt

0.4.0 almost working

Syntax of patterns changed (and not documented yet).
It is now:
 match p with [ _ => p | ... | _ => p ]
(use lambda-abstractions for dummy arguments). Hmmm...

Wildcard patterns implemented in case analysis. The following term is now
accepted:

 match n with
  [ A => O
  | B m => m
  | _ => O
  ]

we use ulex08 not ulex

bug fix in injection e relocate term

neg => Qneg :-)

true and false were swapped!

flase => false :-)

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).