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

now baseuri is needed in each file (and its redefinition is forbidden)
added exception prettyprinter

fixed some errers in the save/cancel ...

catches more errors

does_not_occur unexported since it did not have the expected semantics

fixed save/exit stuff

fix

the error_report window is now properly closed

Removed a dummy "let ... in" that was there only to show a bug (now fixed).

Stupid bug fixed in the refinement of let ... in

Informative message corrected: MatitacLib.go () is now redefined as the more
concise go ().

fix

better message

lapply improved

matitatop.ml is now a simple invocation of Toploop.loop and .ocamlinit is
responsible to call MatitacLib.go or MatitacLib.main.

 Cons: .ocamlinit is more dirty
 Pros: it is possible to trace something even before doing a drop!

lapply improved

New solution: instead of using matitatop.bootstrap we prefer a local .ocamlinit.
 Pro:  no need of doing the weird "#use matitatop.bootstrap" by playing with
       ocaml internals.
 Pro:  local definitions and #opens in matitatop.bootstrap were lost. They are
       preserved in .ocamlinit.
 Cons: .ocamlinit must be in "." or in $HOME
 Cons: it can interfere with other .ocamlinit

In case of EOI the "go ()" loop must exit!

matitatop

More complete bootstrapper.

* new binary matitatop
* command drop enabled for matitatop.
  Once dropped use MatitacLib.go () to enter again the matita toplevel.
  Use #trace and similar stuff for debugging.
  Add printers for abstract data types in matitatop.bootstrap

  Enjoy!

added Drop

misc -> domMisc

fixed bug in response first line parsing (arbitrary reason phrases are
now supported)

added "are you sure you want to quit with usaved script?"

New argument for LApply: the ident for the generated hypothesis.

New argument for LApply: the ident for the generated hypothesis.

changed get_pair interface, now supports different unmarshallers

added get_pair method

moved discovery of METAS dir to configure.ac: script.sh no longer needed
when invoking make in subdirectories of ocaml/

bugfix: uses awk instead of cut for splitting query output (no more empty string)

New tactics.

replace generalized to patterns

1. interface of replace generalized to patterns
2. implementation commented out (for a little while)

A few other tactics made available to matita.
A few tactics (change, fold, replace) generalized to patterns.
The argument of clear and clearbody is now an identifier.

A few other tactics made available to matita.
A few tactics (change, fold, replace) generalized to patterns.
The argument of clear and clearbody is now an identifier.

WARNING: the implementation of change, fold and replace has been commented
out to generalize them to patterns. To be committed soon.

clear already exists

added autosave and * (modified feature)

...

New argument (the identifier) to generalize.

New argument (the identifier) to generalize.

New argument (the hypothesis name) for cut.

New syntax of auto: auto [depth = n] [width = m].

...

fized disambiguation of LApply

* the auto AST now has the width
* a bit of code clean-up
* more tactics made available to matita

support for _ in binders, and a more coplex pattern that should help if
patterns will be used on subterms.
match pattern, term with
| Binder Anonymous, Binder name -> recursion
| Binder name1, Binder name2 when name1 = name2 -> recursion
| Binder name1, Binder name2 -> []

More tactics or tactic arguments made available to matita and a bit of code
cleanup.

* auto_tac removed (it can be found in CVS)
* auto_tac_new renamed to auto_tac
* TacticAst.Auto ported to auto_tac[_new] (i.e. width added)
* MetadataQuery.hint removed (only {new_,}experimental_hint were used)

* More tactics are now available to matita.
* Code reordering (match branches are now in alphabetical order)

More tactics are now available to matita.

fix

more complex

1) moved select and pattern_of from cicUtil to proofEngineHelpers
2) select now returns a couple (context, term) so that we can build the right context from each returned term

Nicer output for the "make tests*" commands.

more detailed but less verbose and annoying report

fixed LApply pretty printing

minor fixes

the web interface for the benchmarking system

first working (?) version of lapply

firs wrking (?) version of lapply

lapply tactic continued

new implementation (due to paths).
terms found by select (that may be under some binders) are delifted to the
context and, once reduced, lifted back.

stupid rename

now we use rplace_lifting_csc since the what must NOT be lifted

fixed select (not Implicit (Some `TYPE) is handled)

fix

fix

New implementation of experimental_hint/auto (called new_experimental_hint) that
dramatically cuts down the total time in certain cases. The idea of
new_experimental_hint is to take in input the universe (the list of uris that
occur in the signature) and to prune the results using the universe in place
of the signature. Thus in place of doing a lot of sigmatches a sigmatch is
done just once at the very beginning.

NOTE: to reduce the size of the universe the empty set of constraints is
not considered.

fix

fix

snapshot

Bug fixed: select => select distinct (since the ors in the where patterns
used to generate duplicates).

shanpshot

fix

fix

nigth-bench snapshot

matita.conf.xml.sample now has a @@OWNER@@ so that sed is easy

added a getter maps updater

cicPxpParser.ml*, cicParser2.ml* and cicParser3.ml definitely removed
in favour of the cicPushParser.ml* (renamed to cicParser.ml*)

first snapshot of the night-profiling

Small improvement in extracting suffixes.

New functions UriManager.uri_is_var, UriManager.uri_is_con.

Asts generalized: a lot of tactics where restricted to identifiers in place
of patterns or terms.

debugging printf removed

added various profiling statistics...

Much simpler (and slightly more performant) implementation of the UriManager.

aded prifiler factory

Added Z, Zplus and its properties.

Tactic discriminate activated in matita.

The discriminate tactic accepts a term, not only an identifier!

1. Tactic generalize ported to patterns and activated in matita.
2. slightly improved syntax for patterns
3. new test for "hand implemented" inversion (that uses induction instead of
   case analysis)

Tactic generalize ported to patterns and activated in matita.

1 .Tactic generalize ported to patterns and activated in matita.
2. new syntax for patterns:
   "in H0 [: ty] ; ... ; Hn [: ty] [\vdash ty]"
   where the list of hypotheses may be empty

reverted to previous version, as it worked better...

fix

local use of OCAMLPATH so that ./script.sh should not be needed anymore

restored local usage of OCAMLPATH so that ./script.sh should not be needed anymore