This commit was manufactured by cvs2svn to create tag
'LAST_BEFORE_NEW'.

*** empty log message ***

new signature of auto_tac, with a new optional argument "full", to invoke the
new paramodulation

added apply_tac_verbose_with_subst, returning a Cic.substitution instead of a
substitution function, needed by the new paramodulation

added binary version of coq.moo and the corresponding source version

removed textual version of coq's moo file

MatitacleanLib.remove_baseuris will remove empty directories.

permutation.ma added to the repository.

Small bug due to case unsensitiveness in the check function.

changed default divide notation to a/b

bugfix: reash uris embedded in cic appl patterns

- added integrity checks on .moo files
- removed a lot of auxiliary functions from MatitaMisc since they are now part of our extlib

better name for a theorem

added magic numbers
they must be increased each time the data structures dumped in .moo file are changed!!!!

set extlib findlib dependencies

implemented the first bunch of useful functions

Mysql ==> HMysql

New module HMysql (to abstract over Mysql and make profiling easier).

New module HMysql (to abstract over Mysql and make profiling easier).

changed .moo format on disk: no longer plain strings, but ocaml marshalling of GrafiteAst.Command lists

More profiling code.

CicUtil.profile ==> HExtlib.profile

CicUtil.profile ==> HExtlib.profile

...

bugfix: evaluation of object commands is now atomic wrt status (including CicEnvironment, metadata, and the heck ...), either it succeed returning a new status or raises an exception leaving the status unchanged

"verbose" argument of remove is now optional (default false)

Less feedback during removal of objects.

...

Too many OPTIMIZE TABLES (because of a very stupid bug).

save_object_to_disk profiler fixed

Profiling code removed.

several "INSERT VALUE" ==> "INSERT VALUES" (more efficient)

Profiling code removed.

avoid generating useless parens in mathml contextes that do not require them (e.g. exponent, fractions, ...)

removed a line of dead code

Dead code removed again!!!

avoid pattern matching on attributed terms since this loses attributes

fix

universes are saved to disk

The disambiguation now returns the aliases diff. It used to return the
new aliases and a slow diff operation was performed later on.

added universes list handling

added universes

added parsing of Type:N

a wrong exception was raised

bugfix for uminus notation, prints parens where needed

added support for universes uri ".univ"

The disambiguation now returns the aliases diff. It used to return the
new aliases and a slow diff operation was performed later on.

log.ma renamed into ord.ma

The new_aliases argument of the functions alias_diff and set_proof_aliases
used to be a whole environment. It is now just the diff! Much more efficient!

A few changes to factorization and gcd.

Environment replaced by lists of domain and codomain items.

More notation here and there.

More notation here and there: \sup, \divides, \ndivides, !

* Added divides and ndivides
* Removed sub and sup

'!' is no longer a decorator (to allow a reasonable notation for factorial).

More notation here and there.

Profiling messages grepped out.

...

Dead code removed

More profiling code.

This commit removes the slowest identity function ever implemented!

We do not longer generate inner-types and inner-sorts for XML files generated
by matitac. We will have to implement a -export flag to matitac to generate
them. This represents yet another important speed-up.

We do not longer generate inner-types and inner-sorts for XML files generated
by matitac. We will have to implement a -export flag to matitac to generate
them. This represents yet another important speed-up.

ported to the new parser interface (Ulexing.lexbuf instead of char Stream.t)

uses ligatures (as a sample)

added ligatures support

rebuilt

clean_and_fill optimization

...

bugfix on proof construction

All the debug_print are now lazy.

More debug_print made lazy.

1. profiling code added
2. debug_print made lazy to avoid computation of the argument when profiling
   is disabled. This really speeds up disambiguation!

Profiling did not profile functions that raise an exception!
Fixed.

...

More profiling code added.

More profiling code inserted.

added non-builtin notation for exists
actually, the parsing rules is built-in, while the pretty priting one is not

changed ast representation of exists

pretty printing of literals is now subject to the debug setting

changed ast representation of exists, now an 'exists simble with a lambda child is used

bugfix in default magic handling: consider as having option type only names
which appear in the some branch and in the none one (previously all names
appearing in the some branch where considered optional)

- bugfix: eta abstractions ignores attributed node while counting lambdas
- permit pattern matching on attributed asts (since attributes are transparent to pattern matching)
- wrapped with assert false some unsafe function invocations (e.g. List.map2)
- removed reset_href (no longer needed)

more refere to bindings in env type definition

fixed matitadep: now it should consider ALL depndencies

added a minimal parser to extract informations relevant to dependencies calculation

...

all initialization code is now in the new matitaInit.ml module.

matitadep now parses notation.

development windows now avoids doing an anction selecting no developments

* Obsolete debugging comments removed
* Debugging comments by Andrea marked with "Andrea:"

Notation for "ex" introduced. It is the same as the notation for forall,
but it uses \exists.

NOTE: there is a bug now in cic_notation. The notation for ex is parsed, but
it is not pretty-printed correctly!

...

More profiling code.

Great speed-up in alias_diff (about 3x).
NOTE: alias_diff is still quite slow (e.g. 2.4s in the processing of
factorization.ma). This function really deserves to be got rid of.
(Moreover, this is possible and not that difficult)

A bit of profiling functions added here and there.

Spurious interpretation removed.

Profiling disabled.

...

This commit (partially) removes a big source of inefficiency (at least for
the select function and the rewrite tactic): CicUnification.UnificationFailure
exceptions were enriched producing (in a very expensive way) a nice error
message. However, the expensive error message is useful only when it must be
shown to the user. Very often this is not the case. Thus I am now postponing
the production of the error message, changing the type of the exception.
NOTE: this kind of improvement can be applied everywhere in the code!
At least it should be applied to functions that can normally fail (e.g.
unification, refinement, convertibility, type checking, etc.)