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

added $(NULL)

fixed +1 numbering (added when the memory consuming fold_right was committed)

removed memory wasting foldright

string -> uri

use of discrimination trees instead of path indexes, for a little
performance gain

trie structure implementation

some optimizations...

testing...

*** empty log message ***

discrimination trees

limited-resource-strategy implementation (now working!)

path indexing integration, limited-resource-strategy implementation (not yet working)

path indexing integration

path indexing working!

fixed increase/decrease size feature

removed!

support for goal patterns

uses new pattern concrete syntax

added support for goal patterns

concrete syntax for goal patterns

added support for patterns current goal

changed select so that it returns a list of pairs <number of binders crossed, term>

profiling experiments...

more strings to UriManager.uri

many strings that are supposed to be URIs are now UriManager.uri

removed spurious entry gtkrc

Locally implemented print_context replaced by CicPp.ppcontext.

A cleaned version of auto_tac_new.

added depth and width (optional) parameters to auto_tac_new

uses auto_tac_new instead of auto_tac

Dead code clean-up.

Dead code for packing/unpacking (usually just a big hack) commented out
(hopefully forever).

Dead code clean-up.

added decrease and increase font size fantafeature

added utility to dump some tables of the db on mowgli
(useful to export metadata to laptops)

matita.conf.xml added

removed again (I added it by error :-(

* parsing errors in tests were not detected and the rest of the file was
  ignored!!!! Tests fixed
* a few interactive tests moved to tests/interactive to avoid regression
  testing over them (for now...)

DTD for attributes revised.
New syntax:
 <attributes>
  <class type="..">
   ...
  </class>
  <generated />
 </attributes>
where the ... are the arguments of the class and the class and generated
elements are optional. For the "elim" class the only argument is the SORT.
For the "record" class the arguments are a list of <field name=".."/>

Syntax of <attributes>...</attributes> improved to allow arguments for
classes.

DTD for attributes revised.
New syntax:
 <attributes>
  <class type="..">
   ...
  </class>
  <generated />
 </attributes>
where the ... are the arguments of the class and the class and generated
elements are optional. For the "elim" class the only argument is the SORT.
For the "record" class the arguments are a list of <field name=".."/>

The `Record class now records also the name of the fields
(used to generate the projections)

a parser error is now logged as an error!

Bug fixed: parsing errors were ignored by matitac since the EOI was not
required to terminate the list of commands!

Bug fixed (that used to throw away a metasenv :-(

fix

renamed clientHTTP to http_getter_wget

we no longer use pxp

support for the new tactics lapply and fwd
used in forward reasoning

enable static linking of C stub code

version 0.7.1-1

- better printing of modifiers
- quit on window destroy

beginning of the tactics lapply and fwd
used to support forward reasoning

sync with new typecheck prototype (no more univ graph)

...

apply_tac used to calculate the type of the term before generalizing on explicit name subts

are_convertible on MutCase was no longer checking the match arguments
convertibility.

ported to latest registry interface

- support for multiple bindings of the same key, accessible via get_list
- changed get_opt interface so that marshallers/unmarshallers are needed
  instead of getters/setters

Refinement of CurrentProof did not check whether the type is a type.
As a consequence it was possible to do "theorem t: 0" :-)

Big commit and major code clean-up:
1. added a refine function for objects
2. added a disambiguation function for objects
3. MatitaEngine now uses the disambiguation function for objects
4. added CicTypeChecker.typecheck_obj to typecheck an object and add it
   to the environment

comments syntax changed

incomplete proof completed.

use META helm-registry package, load sample.xml and open Helm_registry

now something works...

* no more %% comments
* parsed comments must start with "(**b" where b is any blank
  and must be termianted by "*)"

No more %% comments.

parentheses allowed inside comments

test_lexer and test_parser compiled by default

uses XmlPushParser instead of PXP