New implementation of the proof-checker daemon: there is now
only one sequential (= non concurrent) proof-checker that process
one request at a time. The next big step will be to make it re-entrant.

CicCooking.init() must now be used to initialize the proof-checker library.

A .cmo file inside a .cma is linked iff it is referenced at least once.
This was not the case for cicCooking, that simply worked using side-effects
(i.e. registering one function of him to cicEnvironment).

So, I have created a new init function to initialize the wall proof-checker.

LetIn reduction (alias zeta-reduction) is now performed during whd.

LetIn was missing.

* .mli added where needed
* Install and uninstall implemented
* Makefile improvements

configure.in now used (just to check that ocaml and findlib are there)
Very small bug-fixes.

META files are now automatically generated from META-*.src files.
In this way all the hard-coded file paths have been removed.
Installation and uninstallation (still not implemented) should be also
easier.
Moreover, an error in a sub-directory now stops the whole processing.

First version of fix_params into CVS.

First versione of the proofChecker into CVS.

param.annotations was yes or NO. It is now yer or no.

annotations: was yes or NO. It is now yes or no.

First release of cicAnnotationHelper in CVS.
Uses the new HELM OCaml libraries.

.depend must be in the repository

New implementation using the new HELM OCaml libraries.

New implementation that uses the new HELM OCaml libraries.

1) .cma/.cmxa used to simplify META files.
2) Common parts of Makefiles factorized into Makefile.common
3) Makefile added

.cvsignore and .depend forgot

HELM OCaml libraries with findlib support.

initial checkin

Readme for the debianize.helm stuff.

Debianize.helm stuff.
Now you can check out a cvs revision and obtain a *clean* debianized source
tree executing "debian/debianize.helm".
Moreover the generated debian packages are native debian packages.

Synced debian dir.

Removed from debian dir.

Synced debian dir.

added config.sub and config.guess so that the package is ready for Debian

Content-type for MathML Content "fixed". Why was it broken?

out of sync w.r.t. configuration.ml

Underlining of hyperlinks removed.

mkMetaTheoryURL(): param.embedKeys() forgot.
Code improvement.

Changed version number to 0.2.1

BUG FIXED:
An maction with only one child does not have the same semantic
of an mrow. E.g.: when I click to un-expand a node, the first enclosing
maction is the one I am acting on. If it has only one child, nothing
happens. So, if an maction with only one child is put inside an maction with
two children, the inner one stops any possibility to unexpand the outer one.

Checks for mlminidom and lablgtk added.

Some spourious files removed.

...

.cvsignore improved

Disequalities chains for algebra. First draft.

Distribution improvements.

Now automatically generated from Makefile.in

No more used.

First commit towards the 0.2.8 version.

Bug fixed

Bug fixed: $< confused with $^

missing macro

HTTP_GETTER_URIS_DBM added

HTTP_GETTER_SERVERS_FILE introduced

Bug fix: changed "prefix" dir in install target.
Minor changes in debhelper usage.

Changed policy standard version.

Removed INSTALL (not needed) and NEWS (0 sized) from document list.

Remove template like string that lintian hates.

Set DH_COMPAT=2 (instead of 1).

Set section field. Changed maintainer field.

Changed maintainer field and set section field.

Removed temp files from repository.

Small improvement.

Simplification.

0.0.2 ==> 0.2.0 ;-)

- Check for ocamlfind added.
- .cvsignore improved

Unused variable removed.

mlminidom 0.0.2 for minidom 0.1.3

another small bug fixed about the pot

Bug fixed.

Required by the new getxslt method implementation.

Required by the new xslt_index.txt implementation.

Absolute URL to the Getter removed thanks to the new getxslt method
implementation.

No more absolute URLs: the getxslt method of the Getter is now
used uniformly.

Version number updated.

Bug fixed. The bug used to lead to divergence in certain cases (e.g. limit_mul).

- modified /getxslt method, now stylesheets are downloaded on the fly
  and may be kept on various servers
- uncommented /getdtd method
- removed /getstyleconf method
- changed semantics of dbm variables, now ".db" suffix must be present
  in environment variables that reference dbm files

Added ".db" suffix to urls_of_uris default value.

The stylesheet to create graphs are now applied to the result of
the new getempty method of the getter.

Never really used. Functionality eventually replaced by the serialization.

Better error handling when port is not available.

Version 1.2.1beta => 1.2.1

- Stylesheet exceptions now printed in red.
- Load of an already loaded stylesheet now ignored (was interpreted as
  reloadin before).
- Version renumbered as 1.2.1beta.

Code cleanup: more code sharing achieved.

Bug fixed: xsl:import not first child of xsl:stylesheet.

Bug fixed: unbound variable.

Added "/getempty" method.
----
Syntax: "/getempty".
Answer: a minimal valid XML document.
Currently, the returned document is as follows:

  <?xml version="1.0"?>
  <!DOCTYPE empty [
    <!ELEMENT empty EMPTY>
  ]>
  <empty />

----

binary ignored

.deps ignored

- new handling of links
- no more conflict between links and actions (links have precedence)
- cursors now handled by helmpot
- fixed problem with pot cursor

- added method to check for an attribute in a given namespace

Code improvement: more code shared.

Small bug fixed.

The body of the variables was not printed.

indent="yes" in xsl:output removed to impreve performance.

indent="yes" in xsl:output removed for performance increase.

The same patch I have applied in the previous commit to m:ci has been
applied to m:mn.

The patch of Irene to allow MathML presentation inside <m:ci>
was not correct. As a consequence (but there were worst ones)
hyperlinks were not created to sub-scripted identifiers.
I have changed the patch. Though, I am not sure it is the correct one.
In particular, what happens if I put content markup inside the m:ci?
(It was recursively processed in the original stylesheet)

Workaround replacement: instead of a litteral URL (path on disk), a litteral
request to the Getter on phd to resolve the URL.
The real problem (avoiding at all the thing) is still to be addressed.

Bug (that I introduced in my last commit to solve the problem of the
free variable $id appearing everywhere in the notation for LAMBDA) fixed.
Now hyperlinks should be generated correctly.

...

GPL licence added

.cvsignore added

Xalan-J_2.2.D3

xerces required by Xalan-J_2.2.D3

GPL licence added.

Version 1.2 ==> 1.2.0

New version for UWOBO 1.2.