OCAMLPATH is not overrid if already defined

ensure connections get closed after having been served

ensure connections get closed after having been served

bugfix:
- properties where applied and then discarded
- useless assert false removed

ensure connections get closed after having been served

ensure connections get closed after having been served

bug fix: use an (un)marshaller for get_opt instead of a getter

OCAMLPATH is no longer overrid if already set in current environment

Bug fixed in fresh_name_generator: the function used to fail on beta redexes. Fixed trivially without
introducing yet another whd.

added (TODO) section on tacticals)

weak equality on meta used when replacing.
updated to the new goal_proof

added the rule field to goal_proof.
fixed the SupL proof generation (but I think the fix should not be here)

- fixed a bug in unification (not sure in the right way)

CALS tables enriched to make (crappy) docbook stylesheets happy.

Documentation fixed.

New documentation.

More documentation.

More documentation.

Recently introduced bug in CicRefine.eat_prods fixed: a whd was now missing.
Added a test to verify the performances of refinement.

Syntax highlighting for focus/unfocus

Great optimization for eat_prods: if the type of the head of the application is meta_closed,
the construction of the spine of Prods and relative unification is skipped.

1) variables occurring only in proofs anre not relocated
2) during unification the resulting metasenv is cleaned of duplicates
   (duplicates can only be variables in proofs, not in left/right)

Profiling code removed.

Bug fixed: the syntax "?n" used to be broken. It tried a string_of_int "?n".

More documentation.

More documentation.

More doc

added a file useful to load all notation
(use include' and not include).

Added debug menu item to restrict disambiguation to the first pass only.

Axioms are not allowed with the syntax: "axiom name: type.".

svn:ignore fixed (again)

svn:ignore fixed

matita.txt updated

added important comment

fixed LetIn proofs

added again stuff for profiling

added dependency on Str

...

added stuff for profiling macros

- code cleanup, especialli in Indexing where all the goal related functions have
  been revised
- proofs are now factorized with LetIn
- support for profiling

generation of existential variables fixed

removed prerr_endline.

commented out a line to help paramodulation.
now if 0 goals are open every tactic is vacuosly performed

fixed wrong calculation of free_metas

removed a bad prerr_endline

removed prerr_endline

removedx a prerr_endline

fixed demodulation of goal

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

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

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