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

auto rewritten with only one tail recursive function.
this allows to have a GUI to drive the procedure.
a new measure size has been added, and width changed its meaning.
a bunch of unfold lt added to library_auto.

OPT tests restored

more informations on nodes, fixed a bug on conversion, we use ; instead of . whenever possible in rendering

Wrong invariant: Hypothesis (i.e. lambda-abstractions) can have no
(= None) name (if unusable).

CSC: terrific bug fixed. Enrico commented the application of eta_fix to the body
of a constant, without replacing it with Unshare.unshare (that is done inside
eta_fix). To avoid the bug to happear again, I have renamed eta_fix in
eta_fix_and_unshare.

library-auto removed from tests (too slow even in native code)

CicInspect: a function for counting the nodes of a term has been activated
Procedural: reports on node counting in proof terms are aveilable

Procedural: clear tactics added

PrimitiveTactics: intros _ now aveilable
GrafiteAst      : some refactoring

A few extensions for the moebius inversion theorem

Proof of the moebius inversion theorem

DoubleTypeInference: added a comment on "does_not_occur"
GrafiteAstPp: rendering of clear tactic fixed

...

a bit of sharing and the optimization of not folding trough the metasenv if the to_be_restrincted list is empty

some minor fixes done in cividale (bugfix coming from andrea's branch)

elim with a pattern now works correctly (hopefully)

library-auto is only tested in native code (in byte code it's too slow)

some improvements

SubstTactic: bug fix
RELATIONAL : some improvements on integers

Even if we are at depth 0, we first check in the cache for a solution,
before failing. In the other case the assert false at line 76 of
autocache may fail.

Removed an assert false; everything works again, but something
is clearly wrong (to be fixed).

GrafiteAstPp: \n's finally fixed
acic_procedural:
 - elimination patterns are generated correctly
 - comments on elimination cases added

AMBDA-TYPES: some improvements. subst now fully exploited
developments.txt: added library_auto
RELATIONAL: some improvements. subst now fully exploited
cic_procedural: a List.rev was missing :-p
substTactic: tacticals are now exploited properly

LAMBDA-TYPES: some improvements

Subst is passed in input to apapluy, so no need to concatenate the results

Apply_with_subst now returns a subst with a correct type for the meta.

procedural: bug fixes
matita: some \n rearranged
GrafiteAstPp: some \n rearranged
GrafiteParser: added callback

bug fix in subst tactic

goal ==> focus

Subsumption_subst re-added to initial.

@

Deprecated "goal" removed.

A new test on some non punctuation tacticals.

The declarative rewriting step now tries auto timeout=3 before
auto paramodulation timeout=3. This seems to work better then just
auto paramodulation alone when the user tries to help the system.
This because paramodulation is more confused than helped.

added skip, removed end

Much ado about nothing:
 1) repeat tac end ==> repeat tac
 2) do n tac end   ==> do n tac
 3) "goal n" finally dropped (deprecated, semantics no longer clear)
 4) the AST (in grafiteAst) has been changed to better reflect the
    distinction between tactics (including h.o. tactics, i.e. tacticals),
    punctuational tinycals and non punctuation tinycals (i.e. skip, focus,
    unfocus)
 5) all tacticals are now running properly in every condition;
    but tacticals argument (i.e. tactics occurring in tacticals) are
    disambiguated eagerly and not lazily (to be changed)

WARNING: the code in proceduralTypes.ml has been commented out since I am
not able to figure out how to fix it properly

Bug fixed: off by one array access in the last patch.

developments root are now part of default inclusion paths;
incluson path used to include something is printed (to understand what is gouing on)

added library_auto/ to tests.

fixed paths and prefixes of included files

Interface of the argument to Continuationals.Make greately simplified. The
following functions have been removed:
 - id_tactic
 - get_status
 - get_proof
 - set_goals

changed base uri

initial import

EXPERIMENTAL and _INCOMPLETE_ COMMIT:

Tacticals invoked from the top-level but the ones implemented on top
of tinycals  where not working properly because of several bugs.

The current commit changes the code in quite a few places:

1) there is no longer a function Tacticals.Make since tacticals implemented
   on top of tinycals always instantiated the functor with
   Tacticals.ProofEngineStatus, and the toplevel can avoid any instantiation
   at all since it can invoke tinycals directly on the low-level machine
   (implemented by the functor Continuationals.Make)
2) when GrafiteEngine now meets a punctuation tacticals, it directly invokes
   an instantiation of Continuationals.Make, without going througw Tacticals.
   Instead, when it meets a real tactical, it directly invokes Tacticals
   (where Continuationals.Make is applied to Tacticals.ProofEngineStatus
   and not to the module defined in GrafiteEngine and used for punctuation
   tacticals)
3) most of the tacticals not implemented on top of tinycals were bugged
   (and unused). E.g.: solve always diverged unless it was applied to the
   empty list. All these bugs have been fixed.

The commit is incomplete since:

1) all tacticals not implemented on top of tactics now accept only a single
   tactic as argument (if they require a list, the list must be a singleton).
   This limitation is going to disappear again, but we must change GrafiteAst
   so that an atomic tactical becomes a recursive tactic.
2) Seq and Then are not branched (for the same reasons as 1 and a bit of
   lazyness)
3) several auxiliary functions in the argument of Continuaniolas.Make can now
   be removed since they were introduced for wrong reasons.

The night test now shows the last commits and blames/praises the authors.

more discriminate

handles failures (sometimes you can't inject)

New query result diff.

Only benches with the same result are compared for timing.

Added new query to time-diff the last mark with the previous one.
The query is also the example query below in case you want to change the two
marks.

tassi/sacerdot

"end" keyword added

one more step toward a decent destruct
lifting should now be ok, but handling of wight params is still
shaky