-debug should work better

in eta_finxing: type_of_aux' not called on eta_fixed terms
in doubletypeInference calls to type_of_aux' wrapped because of eta fixing

Ugly solution to the "we proved T that is equivalent to T" problem:
we use pack_coercion (defined into cicRefine) inside doubleTypeInference
(that is well below in the module hierarchy :-(

This is also supposed to be quite expensive (since pack_coercion uses
the refiner and coercion packing is applied to every expected/synthesized
type).

Profiling code commented out.

Some times reduced in a second benchmark.

Utime + Systime used in place of gettimeofday.

added patch to allow agin "match sin ? = ?"

fixed new compilation order

exported pp function for terms

whelp locate now accepts * and ?

whelp macros have now () around args

some fixes for whelp macros (concerning pprint...)

Altri benchmarks.

CicEnvironment is emptied when a size treshold is reached.

Removed negative equations.

links to .opt are now generated in the world target

fix for distro

a bit of shareing

added estimate_size

create directory paramodulation for tests for paramodulation

added another interesting problem for paramodulation

the tactic now returns as open goals the open metas in the proof
subsumption is now used correctly in given_clause_fullred

subsumption fixed and called in given_clause_fullred.

Naif substitution. Removed local context in metas during relocation.
Removed apply_theorems in saturate, replaced by a local check for
identity.

Useless code simplified out.

New benchmark after removal of some profiling code.

Less profiling.

Profiling code for merge_ugraphs commented out (since profiling is much more
expensive than the profiled code).

A few benchmarks on the library of Coq committed.

Added deadline (now 30s) to each test.

Sys.Break used to be captured.

Bug fixed: terms with a Cast used to raise assert false when whd was avoided
by the conversion strategy.

Huge speed-up in conversion: the old conversion strategy is set back.
 1. try to "convert" the two terms recursively without performing reduction
 2. if it fails, do a whd and try again
The overall result on the library of Coq is really remarkable.

#### EXPERIMENTAL COMMIT ####
Added a potentially dangerous ~expand_beta_redexes flag to
CicSubstitution.subst. If used carefully, it enormously speeds up
the type-checking of many theorems (since a very frequent conversion test
happens between a beta-redex and its contractum).

Debugging code added.

removed unif_ty ref

reverted the addition of _ to mistyped names

few bits to debug the benchmark system

deals with colors

more profiling and fixes for paramod

args removed from equalities.
New selection strategy. De morgan: 253 s.

Debugging code commented out.

* trust = true
* better pretty-printing of type-checking exceptions

"Performance bug" fixed: I removed a whd in the does_not_occur function.
Consequences:
  1. incredible speed-up in the type-checking of certain inductive types
  2. "dummy" occurrences (i.e. occurrences that are doomed to disappear because
     of reduction) are now rejected (they used to be accepted). Coq has the
     same behaviour.

Several "try ... with _ -> " specialized.

More robust handling of Control-C.

Flush stdout added in proper position.

ignoring test_library{,.opt}

Recently introduced bug fixed in the kernel: a stack was "forgot" during
reduction of a MutCase.

Unable to parse my own output. Fixed.

% forgot in the output

Serious test for the Coq library added (name test_library).
Input: a file that holds a list of URIs.
Output: the benchmark; the output file is also a valid input.
        In this case the output also prints the differences w.r.t. the
        last execution.
Ctrl-break can be used to interrupt the type-checking of a single URI.
An interactive question is posed to the user to decide if proceeding with
the next URIs or not.

more error messages were on stdout :-(

error message was printed on stdout

Colors are back! :-)

New unification and new matching.

Legend for profiling printed iff something is profiled.

fix

fix

Best parameter setting for de morgan.
-- This line, and those below, will be ignored--

M    tactics/paramodulation/saturation.ml

fix

if DISTRIBUTED all targets require a depend-stamp

:
This line, and those below, will be ignored--

M    tactics/paramodulation/utils.ml

profiler on steroids. added -profile-only to specify a regex to choose the profilings to print

removed mysql_escape that should be ok.... but adds some \ that make mysql
complain

added calls number

removed mention of the "library" target, no longer needed for the installation

fixed timestamp issue on tactics.mli

mock-up code for tactics contextual menu in the gui

Changed the type of compute-equality_weight that now takes also
in input the ordering

go

go

go

added raw query form

done

fix

Renamed SK.ma into bool.ma

Esempi di auto.

Snapshot.

removed \t

go

go

go

fixed wrong log name

ahh.....

tests are now handled with a standard Makefile that does not use do_tests.sh

another step roward the removal of do_tests.sh

removed php-shell scripts

moved to the new table

fix

fixed a bug in the Makefile, generatedGui.mli no more there

one more step toward release and bench reorganization

fix

more work for the release

snapshot for release

added elp to distribution

added check to not clean the standard library, a confirmation is required

Huge commit for the release. Includes:
- getter_storage modifications to honor multiple (overlapping)
  ro/rw repositories
- removes of ~basedir
- addition of the 'publish' matitamake command used to install in system
  tables/directory a development (that is compiling with -system)
- removal of .build,.user,.devel config files (only one is needed)
- fixed make dist/install to strip binaries, install the library with the new
  method
- fixed compilation of the getter daemon
- deletion of grafite misc that is no more needed

Added inversion principle creation for inductive predicates.

Inversion code cleaning.