fixed demodulation of goal

- metas_of_term moved to cicUtil
- fixed proof generation
- added again typechecking of generated proof

fixed typo

existential variables in goal supported

ported to ocaml 3.09.2

ported to ocaml 3.09.2

ported to ocaml 3.09.2

do not export .svn directories

transition to ocaml 3.09.2

fixed subsumption_aux
- (merge_subst_if_possible no longer needed)
- fixed case of use_unification = true

fix

fixed

utf8_macros moved to syntax_extensions.
quoting for inline profiling added

few fixes

CSC & Andrea patch to speedup the process: typeof called instead of Hashtbl lookup

more profiling and less assertions

better exception

hashtbl on cic terms is a bit faster

- new given_clause
- support for a set of goals in OR
- restored superposition_left (even if not called)

better way of generating multiple pages XHTML output

- Removed old proofs
- Equality.ml splittend in to subst.ml and equality.ml, the former only for substs
- patch to kill passive generated from an active that is dropped
- fixed deep subsumption

generation of more than one theorem per file fixed

added a couple of points

todo list about doc

more work to produce well formed .ma files

fixed some bugs

full script generation

fixed some pp stuff

...

removed shift-reduce conflict

added parser (and future converter) of tptp files

Bugs fixed:
 * the dependency parser no longer fails when an incomplete "include" or "set"
   are met
 * ask_and_save_moo is now performed more lazily and some bugs have been fixed

few more bits for zack

half ported to the "new" module organization.

types2006 patch

New version of deep_subsumption

goal demodulated with new

new pp function for proofs

eq_chain

more transitivity on proofs

Equality chains.
-This line, and those below, will be ignored--

M    acic_content/acic2content.ml

Added is_trans_eq_URI and is_sym_eq_URI

Build_proof_goal does not return the metasenv any more.

fixed demodulation_goal (used to return always false)

removed ocaml equality on equations

more cleanup

cleanup of saturate

added a new type for proofs.

added a whd (nodelta) in the carr function used by the refiner (in the eat_prods case)
to get the carrier of a coercion. this is useful in case of terms generated by paramodulation
(and we want to refine the proof letting the refiner add symmetry steps)
where we have ((\lambda x:A.P(x)) t) === P'(t)
and P/P' is M=N/N=M

Bug fixed: "paste as pattern" now pastes the full pattern (e.g.
"in H:(? %)"; it used to paste "(? %)" only)

Patch to avoid double execution of whelp queries reverted (since it seems
that queries are NOT executed twice without the patch (!?!) and with the
patch the query is sometimes not executed).

uft8 string length bug fixed (Ctr-Alt-. did not work properly any longer)

multi-instances aliases are compressed to single instances if possible

duplicate check for coercions when added to Db

alases instance not printed if 0

the same utf8 bug as before

fixed another utf8 string length bug

added minimal euristic for generic terms carrier comparison

to tired to write a message.

added include' to include everything but preferences (aka aliases)

partially fixed  boxes in rewite

added keyword include'

-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.

Researcher -> Lecturer

fixed typo

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