better comment for kernel wrappers

a better error message

- Added DisambiguatingParser (that abstracts both the parser and the
  disambiguator used)
- Added ChosenTermEditor (used to swap quickly the editor used).
- moved disambiguate.ml* to oldDisambiguate.ml*

...

removed useless -thread switch

ported to latest lablgtk2 snapshot

added false test

- added -thread switch
- reordered modules

build also cic_textual_parser2

updated

added dependency to lablgtk2.glade

added -thread switch and dependency on lablgtk2.glade

moved disambiguate module away

(temporary, waiting for abstraction over disambiguators) ported to Andrea &
Zack's disambiguator

added ChosenTransformer

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