ogroups almost finished

snapshot

snapshot

End of groups :-)

snapshot

- ProofEngineHelpers: namer_of moved to GrafiteEngine
- DestructTactic: unexported destruct_tac now uses lazy terms

previously hidden simplifications (in old destruct) added

some work till the need of redoing all groups based on excedence

since there is no more tab, the modification of the current file is in the window title

- destruct tactic: automatic simplification in case of failure removed
- library scripts: changed accordingly
- LOGIC: injection lemmas for the coercions added and applied where neaded

Note: destruct does not whd the equality argument as the old subst did

removed ugly printing

ordered_sets are built with excedence

added ordered sets

renamed ordered sets into excedence.ma

relocated

removed dust

HIDDEN (since glade do not read out file properly anymore) tactic bar and
outline notebook tab

new file with some relations stated in Type

ordered set is over, much new stuff coming from a coreflexivee/cotransitive
execedence relation.

refactoring

old subst tactics removed. New destruct tactic used instead

a) Detection of existential types now implemented
b) New heuristic for pretty printing of type definition arguments.

More correct (but still bugged) implementation of type definition.

Dead code removed.
More ocaml keywords.

snapshot

...

- subst tactic keyword removed from highlight syntax tables
- svn:ignore property fixed for Base-2 devel

Trivial bug fixed in type inference of LetIn source types.

xxx

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