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

RT_BASEDIR changed to a sensible path

broken list fix

fixed a list.nth called on a too short list

...

added generation of hne and heq problems

better simplify

simplify has a brand new semantics!
replace_lifting passes a context to the comparison function
(but in the case Fix/CoFix is incomplete)

subst tactic put in a file on its own

closed all axioms

HACK for indtype checking

fixed case

set -> type

...

...

...

match x in IDENT and not TERM

still not completely working but at least non dumb destruct

you can case even if only a right appears... so, substituting them for metas is wrong, rels are better

...

eval_from_stream is now tail recursive!

pattern with match fixed

many printings added

fixed the pretty (notation aware) printer

alpha equivalence fixed: in the case "meta against meta" we did not recur on theexplicit substitutions. The case "Type against Type" and "Implicit against Implicit" need to be checked. Are we really sure that structural equality is enough?
(when we compare universes and implict annotations)

alpha equivalence test factorized and moved to CicUtil

new case implementation

Procedural: some improvements

Procedural: refactoring

Cic2acic  : added some debugging information
Procedural: some refactoring and improvements

added some tests for cases

hopefully fixed cases implementation

Optimizer: refactored according to its formal description

Serious bug fixed: a variable was captured during unfolding of Fix, resulting
in the context of the return type of mutually recursive definitions being
lifted for each function but the first one!

added eta expansion to avoid universe inconsistency.

Several instances of the same bug fixed at once: when processing a Fix,
before adding the types to the context (to process the bodies), the types
must be lifted. The simplify tactic is still not working propertly.

Debugging code removed.

elim tactic: it needs two arguments, a term as well as a pattern
CicReduction: head_beta_reduce now can take the number of beta-redexes to reduce
Procedural: refactoring

New contrib moebius.ma.

Extensions required for the moebius function (in Z).

Role of
 - replace
 - replace_lifting
 - replace_lifting_csc
clarified with comments. None of this function is the inverse of subst :-)

elim tactic: now takes a pattern instead of just a term
             works as before for now. the pattern wil be activated soon
Procedural:  cleaning up
ProofEngineReduction: new subst_inv function exactly inverts subst

Few theorems added.`

new version of div_and_mod

Capturing Invalid_argument inside pp (otherwise we cannot even
see what's wrong *) wrong.

case to elim conversion works fine