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

cvsignore for html documentation dir

- added ocamldoc documentation in debian package

- fixed wrong @raise ocamldoc tags

- added targets relative to ocamldoc doc generation

- bumped version to 0.0.5

- removed old entries from TODO
- updated changelog

- added support for multithreaded daemons
- added a generic 'respond' function, used also as low level for other
  respond functions
- added support for chdir in a given document root before starting
- added toString method to response objects

...

First version of the stuff to create the DB.

The notational stylesheets from CIC to MathML Content are now automatically
generated by Di Lena's meta_style. Rember to add a new entry to servers.txt!!!

First version of Di Lena's stylesheet generator (for the HELM DTD).

typo fixed

*.yy.c removed

*.rdf ==> *.xml

...

<h:Object> is now repeated every time a MainHypothesis (with its depth) is
printed. The RDF file gets a bit bigger, but lexical analysing it becomes
much easier.

Bug fixed: refSort were exported (as refObj) also when occurring InHypothesis
and InConclusion.

rdf:parseType="Resource" added to backPointer

* New metadata for refSort and refRel
* New metadata schema

TODO list

- changed invoked daemons for proof checker, draw graph and uri set
  queue to ocaml ones
- bugfix: use different pid files for old a new libraries daemons

added env var DRAW_GRAPH_DIR

- get working directory from env var DRAW_GRAPH_DIR
- in case of make failure (which in turn usually depends on uwobo's
  failure) return an error message in HTML format
- bugfix: return html file instead of ... nothing :)
- bugfix: print real current directory

- http debugging value copied from daemon debugging value

<h:depth> must precede <h:occurrence> (to make metadata inversion easier)

bumped version to 0.0.4

Debug code removed.

- bugfix: perform GET parameter parsing on HTTP encoded urls _then_
  decode them
- removed now useless pair_of_2_sized_list

mqint patched (compilation warning removed)

Minor bug fixes:
 - forward_{rel|sort}.rdf ==> forward_{rel|sort}.xml
 - forward_{rel|sort}.xml were not valid XML documents

- added a lot of debugging messages
- changed semantics:
  - overflow check is now before already_in check
  - old uris are not forgotten

Now Pattern module really exists in repository.

Pattern module added.

added ocaml version of draw_graph and uri_set_queue

New metadata for sort and rel.
New metadata schemas.

Relation: inverse switch added.

Modified Files:
1) schema-h schema-hth: work in progress schemas

generator patched for new semantics with structurated attribute names

structurated attribute names added

bumped version to 0.0.3

renamed tcp_server module in http_tcp_server to avoid future
name clashes

bug fix: reset timeout after processing request in Tcp_server.simple

*** empty log message ***

Added debug flag and debug_print function

.cvsignore for examples dir

- split http_parser module (all code that parse http requests and
  responses)
- split tcp_server module (which contains different [actually 2]
  implementation of Unix.establish_server like functions)
- implemented a tcp_server which doesn't fork
- added ~fork parameter to Http_daemon.start* functions

oopss, I forgot to commit .depend last time ...

backported new pxp module from branch V7_3_new_exportation
Close an incredible bug (Neturl.Malformed_URL) in fully ocaml proof checker.

replaced fun with inverse attribute

added inverse switch for relation and attribute
removed fun

name fix due to changes in libhttp-ocaml (e.g. s/Http\.Daemon/Http_daemon/)

Attribute files added.

Unused files removed.

load http.cma instead of http.cmo

no longer use -pack and Http.*, now interface is the usual Http_*

Now use cm{,x}a

Changed source-package name to "ocaml-http"

Attribute patched: now takes an extra argument of type bool.

Attribute patched with inverse function.

switched to OCaml HTTP module

added ocaml-http 0.0.1

first commit

Fun patched.

bug found:
 - >= is splitted in > or = ,so unification fails

...

Comments removed.

Quotes problem fixed.

MQueryGenerator ported to use fun "objectName"
topLevel        typechecker output was removed

silly debug output removed from stdout

New version of the library added.

xmlns:h namespace "fixed"

New version for the new DTD.

Fun patched but works only in one direction (from the alias to the uri).

proof-checker ported to the mowgli version

Proof-checker ported to the mowgli version.

Better configuration management.

Now esempi/fourier.cic end with a proof!

- used change_tac to change from a->False to ~a just before tac2.

Fix: Ad hoc change_tac may not work sometimes. check what Cic.Anonimous means.

Bug fixed: I don't know what the bug was exactly, but it happened that
the connection was not closed when using some HTTP 1.1 clients (e.g. wget)

mqint.ml patched

topLevel updated to use mqint set_database and get_database

Bug ``fixed'': we do not need to apply sym_eqT since the goal we produce
is already 1^-1 = 1 (while Coq produces 1 = 1^-1).

- matql_interpreter_galax branch removed once and for ever
- added the dependency to natile-galax. You need to add
  /projects/helm/galax/sources/natile-galax-0.1-alpha-installed/lib
  to your OCAMLPATH to make it compile again.

Switching interpreter patched, addedd:
 postgres_db
 galax_db
 get_database

The two interpreters are now both in mathql_interpreter. The one actually
used can be choosed setting a global reference.

No more useful

Old modules (use.ml/mli, eval.ml/mli,...) eliminated.

Switching interpreter.

Comments reindented.

Merge of the new_mathql branch with the main branch:
 - new query language
 - new interpreter for the new query language

NOTE: the galax version of the interpreted is not ported yet (and does not compile)

Merge of the new_mathql branch with the main branch:
 - new query language implemented
 - the locate query is now bug-free (and a _LOT_ faster)

- indentation is now in pseudo-functional style!

- rewritesimpl_tac added in fourierR.ml (wrong location)
- simpl_tac added in fourierR.ml (wrong location)
- "RewriteSimpl ->" button added
- "Rewrite ->" button removed

- write_tac fixed (the list of new goals was empty)
- some new bugs introduced here and there ;-)

A tough test for rewrite.

- bug fixed: some liftings were missing in the implementation of rewrite
- new feature: rewrite now works up to alpha-equivalence

- rewrite extended to handle rewritings with eqT
- equality_replace implemented (based on the new rewriting tactic)

Trivial bug in equality_replace fixed: an exception was raised in spite of
returning false.

New tactic rewrite implemented.
Not tested yet.

- idtac used for debugging removed
- bug fixed: the natural number 1 was mapped to (Rplus R1 R0).
  It is now mapped to R1 (as it should be). This close all the
  residual bugs.

Still to do: we need to close the last open branch using equality_replace,
as soon as it is implemented.