1. "by proof" now allowed as a justification in equality chains.
   It opens a side-proof to be proved immediately.
2. Side proofs restored in equality chains in content2pres.ml

Added ~with_cast to the change tactic.
When with_cast is true, a cast is recorded in the lambda term.

Bug fixed: name in letin was printed as "previous" even if given.

More opcodes (badly) implemented.

List.ma: added function nth (with default value in case of failure)
Assembly: a toy example on proving properties of assembly programs.
 It should be moved somewhere else. It shows HUGE problems with
 simplification and display of (very very large) terms.

New definition of Euler's totient function.
New theorems about sigma_p (invoked with an always true predicate).
Theorem about the sum of totient invocations on the divisors of a natural number.

In order to generate executable declarative scripts, we are now splitting
the "Rewrite" content-level method into "RewriteRL" and "RewriteLR".

Bug fixed in bottom-up conversion.
Since the bottom-up conversion body is put in the applicative context and since
applicative contexts get flattened the test for being in a bottom-up conversion
must be rather complex.

BU Conversion was not generated for Rels fixed. I wonder why...

Nicer layout but possibly more bugged.
We need continuations here to do a good job.

Spurious "we need to prove" at the beginning of Intros+LetTac are no longer
generated.

generic version, specializing generic_sigma_p.ma

generic version

theorems about sigma_p proved using sigma_p_gen

svn:ignore property set

new gcd properties, and theorems for totient, and theorems for totient1

--this line, and those below, will be ignored--

M    minus.ma
M    le_arith.ma
M    lt_arith.ma
M    div_and_mod.ma
M    div_and_mod_new.ma
M    orders.ma
A    propr_div_mod_lt_le_totient1_aux.ma
A    gcd_properties1.ma

some old auto yurned into autobatch

generic sommatory.

removed ugly printings

PoplMark challenge part 1a: new, shorter version w/o equivariance proofs.

better description

better description

here we are, a version that compiles and seems to run

Incompatible syntax problem between MySql e Sqlite3 fixed.

cut is now implemented building a letin and not a beta redex

many changes:
1) fixed many bugs and added support for implicit detection in
   cic -> declarative
2) added a tactic to find a proof rewriting n times with a given universe
   used instead of auto_paramodulation in the declarative language
   (here you know that 1 rewriting step with that lemma is enough)
3) added ESCAPE to sql queries using LIKE, to make sqlite and mysql compatible

sort_new_elems on prop_only

fixed to allow make-dist

added doc for compose

compose now returns a good metasenv

tentative fix

Another optimization, already done for geq.

auto proof are printed in procedural style

new more flexible compose, see matita/tests/compose.ma for a sample

wrong assertion was inserted, now just a warning to know when it happens

Some interesting optimizations to prevent many bad checks.

Profiling enabled again.

removed some refinement_toolkit

new compose tactic, still undocumented.
moved from library to tactics the code for composing coercions.

I do not know why, but
(Helm_registry.get_list Helm_registry.string "matita.includes")
is extremely slow! Removing it from the inner loop really improves performances!

hacks for paramodulation declarative proofs

Final (???) bug fixed.
The fixpoint for n=1 is now reached in 22s.

DOOMSDAY 1.0:
 this is the commit that (partially) allows Matita to understand its own
 output. I.e. the natural language generated is now the declarative language.
 This is probably still highly bugged in most cases.

Bug fixed: wrong id.

Ferruccio has changed the semantics of the old ~pattern argument of elim_tac.
However, he did not fix by_induction_tac accordingly. For now I comment out
the ~pattern application. To be fixed.

More exceptions pretty-printed.

theory_explorer now communicates directly with matitawiki.opt.
Overall time to reach the fixpoint for m=1 changed from 91m to 11m!!!

now the window can be closed also using X

1. Profiling enabled.
2. Dotfile inserted into log.ma for debugging pourposes.

hSqlite3.ml used create_fun_2 to define REGEXP.
this functions is not official, patch sent upstream

added some lines to compile for debugging

added pruning option in autogui

Corrected version od meta_convertibnility_subst.

Bug fixed (hopefully without introducing new ones): when the user clicked in
AutoWin on a theorem that does not generate new goals, the hint was never
found and auto "immediately" failed.

Improved pruning (no propress).

Added a new version of meta_convertibnility that returns the
variant substitution.

1. Now I save a log.ma file that is exactly what is proved!
2. Only three arcs missing in 61s (with a low depth) :-|

log.ma is now created. But it does not contain the exact sequence of things
proved by auto.
width=2 does not seem to hurt!
the graph is now really acyclic (I swear).

log.ma is now created. It records all the tests (both failure and successes).

Yet another assert failure fixed.

More warnings.
More bugs detected by warnings fixed.
auto => autobatch.

added $Revision$

auto --> autobatch

auto --> autobatch

New asserts.
Saner invariant: a not-yet-located node is now put both in the inf and sup
lists.

auto and autogui... some work

auto and autogui... some work

fixed a when that was causing backtrace loss

More assert failures and some bugs (detected by assert failure) fixed.

added some flags to render subproofs (an hack)

All known bugs fixed.
Compilation is now in nativecode.

It no longer generates double arcs between nodes.
Bug: it does not put ii in the same equivalence class as i.

Still bugged.

theory_explorer_do_not_trust_auto.ml is the version that does not trust
 auto. The algorithm is exponential.

theory_explorer.ml trusts auto and requires only quadratic time. Not working
 properly yet.

I am now using tred to remove transitive dependencies from the graph before
displaying it.

1. generation of log file commented out (it gets too big too early)
2. bug fixed in highlighting of the red node

Yet another patch to LibraryClean.
Now we look for URIs to remove both in the filesystem and in the objectName
table of the DB.

HSql.Error ==> HSql.Error of string

prerr_endine ==> debug_print everywhere

Reindented.

Even more color (for new nodes).

deps fixed

Use different colors to understand what is going on.

makefile reworked to make debian package possible

Unlinked nodes are now printed.
The algorithm works only if - is considered immediately. Fixed.

made matita.runtime_base_dir overridable setting MATITA_RUNTIME_BASE_DIR env variable

MATITA_* env variable preserved when publishing a development

changed the way environment variable can interfere with the registry.

added is_writabledir to extlib

added some hacks for the debian package

debian package for matita

xxx.dot improved

Automatic exploration of the theory of intuitionistic interior, closure and
complement.

Slightly more efficient patch.

applyTransformation: added debugging information
makefiles: %.mo.opt now working
developments.txt: added Base-2 devel
acic_procedural: some improvements
 new optimization: atomic let-ins are now expanded

- new devel contribs/LAMBDA-TYPES/Base-2 with the automatically generated
  procedural representation of the proofs in contribs/LAMBDA-TYPES/Base-1
- template_makefile_devel.in: %.mo.opt now works
- acic_procedural: some improvements
- PrimitiveTactics: a part of the elim tactic was factorixed for use by the
  procedural reconstruction

added alternative implementation for hMysql relying
on sqlite3.

In some cases (e.g. JM equality) the inversion principle is not generated
because CicRefine cannot infer a dependetly enough type. Now a warning is
raised and compilation is not stopped.

added a (for the moment) dummy field _subst to ProofengineTypes.proof.
36 file touched ;-)