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

added a test for rewrite under Pi

rewrite tactic: bug fix in rewriting under Pi's:
                the application context of the subterm to rewrite can not be
forgotten

Procedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation

some improvements

Procedural: bug fix

Relational: one file was missing :-)
Procedural: the cic object preprocessor was not added to svn :-)

Procedural  : cic object preprocessor added
depend[.opt]: some fixes

Procedural: now patterns for rewrite are generated correctly

Procedural: some improvements
rewrite tactic: bug fix in hyps searching
TermContentPres: one space added in let-in rendering
prova.ma: new procedural proof of ty3_gen_cast

procedural proof of ty3_gen_cast

"by j let x : T such that P(x)" generalized to allow arbitrary justifications.
The code and behaviour should be cleaned up a little bit.

some improvements

- Procedural: some improvements
- intros n tactic: now tries whd when Pi or let-ins are not enough

decompose: delta-expansion of the type to eliminate now works fine

RELATIONAL: new undecomposable definition of NLE
Procedural: some refactoring
decompose tactic: only types of sort Prop are decomposed now

decompose now works without premises

procedural      : some improvements.
decompose tactic: user provided premise and types removed.
                  The decomposable types are now the non-recursive inductive
  types without right parameters and are auto-detected

acic_procedural: changed module compilation order
TermAcicContent: bug fix in AMutCase
                 the presence of left parametes was not taken into account

small fix to make it compile again

added some code to print the praamodulation proofs with a graph