New function (only partially implemented) to pretty print an Ast at the
semantics level.

added some utility functions on filename suffixes

Use eval_from_stream in place of eval_from_stream_ref to avoid printing the
prompt.

include must not add aliases in the script!

"include" command implemented.

"include" command implemented.

matitaclean splitted in matitacleanLib and matitaclean.

alias declarations are now put in the .moo file.

matitaclean now call getter.ls using a buri with a trailing /

Improvements in matitatop: instead of doing exit -1 it enters the toploop
after a ^C.

Equality tactics are now used in the first half of the script.

Note: it seems that "elim H ?" is more powerful than "rewrite < H ?" since
it is able to discover the value of the implicit argument ?. To be improved.

The equality tactics are now exploited.

All the equalityTactics have now been ported to use both the equality of
Coq and that of Matita.

Note: the only problematic tactic is replace that must pick an equality without
any hint. Right now it always picks the one of matita.

New theorem: eq_ind_r.

cosmetic change: a space removed (to make tests/Makefile and library/Makefile
the same)

fixed bug in proof generation, new weight function to sort equalities, which
gives a huge speedup

may fix the nigtly build

more makefile work

make tests and make tests.opt now call their counterparts in library and tests

The tests are now in alphabetical order.

match.ma removed

* match.ma removed (it is now splitted in several files in library/*.ma)
* Makefile.tests removed (redundant with tests/Makefile)
* make tests and make tests.opt now call the same targets in library and tests

...

conflicting baseuri

matitaclean is necessary!
However, we need a fast ls method for this. Waiting for Zack's new getter...

...

* makefile improved
* new target-schema: *.opt

new targets:
  opt
  verbose.opt

...

New argument: the cleaner.

make all is now nicer

Two targets now:
 make all
 make verbose

make MATITAC="../scripts/do_tests.sh ../matitac /dev/null"
can now be used to benchmark the output

...

Makefile improved

The library of matita is borned! Long life to the library of matita.

ma -> moo in dependencies

more logging information on received request

uses relative OCAMLPATH

now maketests uses matitaclean (but not in the right way)
tests are made in the stupid order, not in the needed one

first snapshot of separate compilation

on is now a keyword (needed in let rec)

added uri_is_ind

matitaclean.opt, matitadep.opt

removed first Cic.term from type equality, added an int (weight of the equality)

...

TacticAst2Box no longer used.

Module TacticAst2Box unused!

count_pattern implemented

More cases implemented in tactic_count.

An interesting test for replace.

replace tactic reimplemented.
It is now able to replace several terms at once.
NOTE: it is still unable to replace terms in the hypotheses.

pattern_of function reimplemented. Now it takes a term and a list of subterms
and it returns the _minimal_ pattern for the subterms in the term.

prerr_endline -> debug_print

Signature of fwdSimpl changed to get rid of a warning.

The replace tactic is now working again. It can now replace simultaneously
n terms.

Signature of fwdSimpl changed to get rid of a warning.

uri_of_string now checks the uri is well formed

matitaclean

New syntax for patterns.

1. change_tac moved from PrimitiveTactics to ReductionTactics
2. fold_tac reimplemented using change_tac

New test.

\vdash added

Syntax of patterns changed again to make it non-ambiguous:
 [in match t] [in sequent_pattern]

in case of performace improvement there is no performace loss message

matitaclean anapshot

proofs are now built lazily at the end of the computation

...

Signature and concrete syntax of fold fixed.

The pattern of a fold cannot have the "wanted" part (for the same reasons as
rewrite)

Signature and concrete syntax of fold fixed.

lapply and fwd improved

Text fixed (due to stricter semantics for naming the binders in the patterns).

The rewrite_* set of tactics is now working again. However, as before,
they do not work yet when the user asks to rewrite somethign also in the
hypotheses.

Bug fixed: a wrong lift made select unuseful when wanted was an open term.

Pretty printing of Cic.Implict (Some `Hole) is now "%"

1. rewrite_* and rewrite_back_* merged into one function
2. signature of rewrite_* improved
3. concrete syntax for the rewrite direction fixed to ">" and "<"

NOTE: rewrite_* is still no longer working.

1. rewrite_* and rewrite_back_* merged into one function
2. signature of rewrite_* improved
3. concrete syntax for the rewrite direction fixed to ">" and "<"

NOTE: rewrite_* is still no longer working.

Oooops. I forgot the convertibility test that makes the change tactic correct!

baseuri put back

The tactic change is now working again. Moreover, it now receives a pattern
in input; moreover it handles correctly the with_what argument when it must
be put in a context different from the one it was parsed in.

A bit of renaming in the code to make it more clear.

...

A simpler implementation of inversion that does not generate the dummy
hypothesis Hcut: 0=0.

buri_of_uri is now #xpointer aware.

added license stuff

better handling of script names

added a debugging helper

Obsolete comment removed.

Stupid bug fixed (a completely erroneous assert false removed).

This commit makes ProofEngineHelpers.select reach its full potentials.
Its arguments are now a conjecture and a pattern and its output is
a conjecture-like structure made of physical pointers to matching subterms
(together with their contexts).

first matitadep snapshot

1. new syntax for patterns:
    [t] [in p]
   where t is the term to be matched and p is the pattern on the hypotheses
   and on the conclusion (whose syntax is not changed).
   All the tactics now use the new syntax.
2. several tactics have been changed to use the new kind of patterns
   (that also have the optional term in them)
3. the signature of the select function has changed to require the context
   (and return a context and not a "context patch"); moreover it performs
   now both the search for roots and the search for subterms of the roots
   that are alpha-convertible with the optional given term (if any)

WARNING!!!
The following tactics have been commented out for a while:
 replace
 rewrite
 change
 fold

1. new syntax for patterns:
    [t] [in p]
   where t is the term to be matched and p is the pattern on the hypotheses
   and on the conclusion (whose syntax is not changed).
   All the tactics now use the new syntax.
2. several tactics have been changed to use the new kind of patterns
   (that also have the optional term in them)
3. the signature of the select function has changed to require the context
   (and return a context and not a "context patch"); moreover it performs
   now both the search for roots and the search for subterms of the roots
   that are alpha-convertible with the optional given term (if any)

WARNING!!!
The following tactics have been commented out for a while:
 replace
 rewrite
 change
 fold

removed profiling function (now a stub is used instead)
added a comment in urimanager

Incredible bug of simpl fixed: the stack (in the terminology used for the
Krivine's machine) was processed in the wrong context. As a result List.nth
(to get a Rel in the context) used to raise Failure in several cases. The
Failure, however, was catched somewhere in the code of matita and the
failure of simpl was hidden in most of the cases.

various updates, removed proofs for now because they are the real bottleneck!!

lapply reimplemented using letin_tac

A few bug fixes. In particular parsing errors in matitatop when a file is
given to process used to result in entering the ocaml mode. Now the user is
left in the matita mode.

fix