abstracted over which transformer gTopLevel uses (ocaml or xslt)

Now applying ocaml transformations to sequents as well.

A few modifications, here and there...

Added all transformations for sequents.

The parser have been made more functional with a trick.
Now there is no more need to save and restore the metasenv.

use "assert false" where needed

added some match examples/regtests

located parse error message

- bugfix: raise an Invalid_choice insteda of a generic exception on
  inductive constructor error
- moved TEST_INTERPRETATION debug message in a better place

added to CicMetaSubst subst wrapper for CicReduction.are_convertible

- added backup target
- use pattern rules instead of anciente prefix rules

- removed some unneeded dependencies from debian/control
- bumped standards-version

Typo fixed.

prettified

use new proofEngineHelpers

moved hard coded uris to HelmLibraryObjects

ported to cicMetaSubst

- splitted into cicMetaSubst
- bugfixes
- better exceptions

bugfixes, typos and the hell

split into this and cicMetaSubst.mli

added CicMetaSubst module for metavariable instantiatiation

better exception and error messages

- bugfix: print metas local context in the rigth order
- renamed string_of_name to ppname and exported it

First version of refine for MutCase, still largely incomplete.

/projects/helm/log moved to /var/log/mowgli

/projects/helm/run/*_mowgli.pid moved into /var/run

Scripts simplified (since now we have only one cluster and only one
stable version of the library).

NuPRL stuff moved.

No longer in use. The official repository for the
stylesheet is now the repository of mowgli.

Branch V7_3_new_exportation merged.

Error message updated.

No more in use.

Typo fixed.

We are now using the standard dot distribution of debian.

Only V7_mowgli left.

Daemons moved to /projects/helm/daemons.

Daemon moved to /projects/helm/daemons.

*** empty log message ***

Several daemons moved into /projects/helm/daemons.

Errore message improved.

Missing package dependency.

snapshot, almost working
TODO:
- domain processing order
- notation generation

added a CSC's TODO comment

added MkImplicit module for meta handling

added Peano module and functions to create natural/real terms

Branch V7_3_new_exportation closed.

mathql listed twice

The searchengine now requires the mathql_db_map.txt.
Added the mathql_db_map.txt file and the new environment variable
MATHQL_DB_MAP.

No longer in use.

Error in the warning message.

added missing depending on (CSC's) helm-cic_textual_parser

removed ui_logger, now in external module logger

added missing dependencies on mathql-*

added logger's META

moved to the logger module

- added logger module
- vertical ordering

moved here ui_logger from gTopLeve

still a working copy, now towards a cleaner implementation ...

added HelmLibraryObjects module

* removed email address

Bug commented out. The comment is also commented.

Big bug spotted: restriction can fail and it was implicitly assumed that it
didn't. Added another comment in the code.

One of the bug I detected (and commented) in my last commit was not a bug.
This commit removes the erroneus comment.

patched

More comments. Some of them may highlight bugs or open issues.

generate gui to temp file in order to catch lablgladecc2 failures

rebuilt

s/Logger/CicLogger/

use ocaml-http instead of netclient for http requests

Makefiles patched

Big bug spotted and commented: the delift function considers the explicit
substitution over metavariable occurrences as telescopic. Instead it is
simultaneous.

* comments improved an possible code weakness (i.e. less than first order
  unification detected) made explicit in the comment and with a warning.

* Reindentation
* More comments

* Reindentation.
* Useless code elimination.
* Debug code elimination.

- ported to new output_html Disambiguate callback
- removed netclient dependency

s/netclient/http/ in dependencies

cosmetic changes

use ocaml-http instead of netclient for http GET requests

- use ocaml-http instead of netclient for http GET requests
- renamed Makefile targets so that all and clean have the usual
  semantics

removed old perl versions of graph daemons

use new METAS/* names

removed ancient "interface" dir

removed ancient lablgtk, lablgtk_gtkmathview

removed ancient mlminidom

removed ancient pxp dir

removed useless ocamlfind query of the netclient package

removed useless "-package netclient" from one of the examples

bumped version to 0.0.9

fixed typo in ocamldoc comment

removed dependency on netclient, use http_client module from ocaml-http

added parse_response_fst_line

- return (or iter on) just http response's body
- s/http_get_iter_buf/http_get_iter/
- commented interface files

added Malformed_response exception

added http_client module

rebuilt

ported to ocaml 3.07

renamed META*.src to meta*.src so that ocamlfind list doesn't list both
src and real METAs

- fixed logging in log window so that spurious html tags are no longer
  printed
- factorized a lot of error handling code in invokeTactics
- moved (and reimplemented) logger class to ui_logger module

renamed module "logger" to "cicLogger" to avoid confusion with user
interface logger

sample script.sh which read META files from ocaml/METAS