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

Unified-Sub: lift_comm completed

contribs: some improvements

contribs: some improvements
Sequent2pres: added some spaces

refactoring

some improvements

Procedural       : some improvements
PrimitiveTactics : tentative implementation of using clause in elim
CicNotationParser: noe declarations of the form (_:t) are parsable

LexiconAstPp: fixed syntax for include
TermContentPres: fixed syntax for letin
lexiconEngine: moved callback from grafiteParser
matitac: -dump patched

unified: some theorems on Lift started

Unified: INC and BEq removed
contribs: added dependence to ../legacy in the Makefile

added option -dump to matitac for persistent macro expansion

Avoid generating invalid names with "'" in the middle of them.

Added toggle for enabling/disabling the conversion from multibyte unicode
characters to TeX when converting CIC terms to textual formulae. The toggle is
under the Edit menu (rational: it's near the paste commands, maybe it should be
added to the GtkSourceView contextual menu too). The toggle governs the
matita.paste_unicode_as_tex boolean registry value. The txt_of_* rendering
functions have been changed to accept a new optional boolean parameter.

The ApplyTransformation.txt_of_term function has been made more robust to
exceptions.

- moved to the view menu toggles for coercion hiding and notation pp
- moved back the high level pp toggle to the debug menu

Exceptions should never escape the final exception handler for the worker
threads. This patch just reduces the probability.

Debugging code fixed. To enable debugging just set debug to true at the
top of the file.

Debugging code removed.

moved the high level pretty printing setting to a toggle menu item of the View menu (with CTRL-P shortcut)

More progress in technicalities/setoids.ma.
I have now reached the final theorem!

Manual for the "default" command updated.

* 'default "equality"' command changed to consider also
  eq_rec, eq_rec_r, eq_rect, eq_rect_r
* rewrite tactic changed to rewrite also in goals of type Set and Type
* more progress in technicalities/setoids.ma

If a pretty printed term spans on multiple lines, then it is printed after
a new line and followed by a new line too.

Important commit:
from now on the pretty printer CicMetaSubst.ppterm_in_context is substituted
with a reference to an high level pretty-printer (now defined in
matita/applyTransformation.ml). In the debug menu there is a switch to turn
it off and get back the old pretty-printer.