mathql interpreter flags can be now red from helm registry

...

uwobo ==> uwobo.opt

...

Stuff moved around.

ENVSCRIPT and mathql_db_map.txt no longer in use.

Removed stuff no longer in use.

helm_registry is already in due to transitive dependencies

The order IS significative. Changing the order (in one of the last commits)
broke the ls method.

typo fixed. Used to break the ls method.

- better error message on "unknown identifier"
- use newer (Andrea and Luca)'s box-based-pretty-printer

fixed cosmetic typos during pretty printing

- bugfix in term grammar: lowered precedence level of "let ... in" so
  that "let x = 1 in x + 2" works as expected
- decent grammar for tactics and tacticals: now with precedence levels
  (no more stackoverflows, hopefully)

catch parse error exception and show them to the user during main loop

patched

batchParser and regtest patched to avoid a non encapsulated connection to the mathql interpreter

Bug fixed: Helm_registry was used not enough lazily (i.e. before loading
the configuration).

added copyright info

removed useless Mpresentation module

moved away tactics and tacticals

added tactics and tacticals (heavily bugged)

added hook for .cma link time options

added tactic and tactical (still heavily bugged!!!)

68080 (that overflows ; -) ==> 38080

fixed typo

New key postgresql_connection_string.

removed (now useless) connection string line

New key mathql_interpreter.postgresql_connection_string.

The PostgreSQL connection string has been moved to the Helm_registry
(key mathql_interpreter.postgresql_connection_string).

Other stuff no longer used removed.

Several no longer used variables removed.

Porting of applyStylesheets.ml to Helm_registry.

Reindentation.

mathql_db_map.txt now retrieved by Helm_registry.

mathql_db_map.txt is now retrieved by Helm_registry.

-linkall removed

- ported to Helm_registry
- ported to the new disambiguating parser of Zack & Andrea

searchEngine ported to Helm_registry.

fixed typo

All daemons are now run in their .opt version.

Any residual reference to tomcat and servlets changed to references to
Web-Services ;-)

- double_type_of: sort_of_prod modified to expect also a meta
- cic2acic: string_of_sort badly patched to return a "?" when a meta
  is found. Note: this solution is not admissible, since it generates
  non-valid XML files (and it may also break other things).

triciclo.conf.xml ==> gTopLevel.conf.xml

More daemons ported to Helm_registry.

drawGraph ported to Helm_registry.

Porting of uriSetQueue to Helm_registry.

proofChecker ported to Helm_registry

- Ported to latest version of Helm_registry

- Uwobo ported to Helm_registry
- Environment variables used only by loadPredefinedStylesheets.pl moved from
  template.* to etc_default_helm_mowgli

Cached moved to /tmp/helm/cache.

Ported to Helm_registry.

...

...

bugfix: top level keys now should work

- Configuration file moved to /projects/helm/etc.
- Configuration file ported to latest version of Helm_registry.

- triciclo.conf.xml.sample ported to the latest version of Helm_registry
- annotations.{url,dir} renamed into local_library.{url,dir}

- more structured configuration file
- commented out save_to since it's not yet implemented for the new XML format

typo fixed (unbalanced parens)

added ocamlinit target which creates a .ocamlinit file

solved a precedence issue between binders and arrows

do not use tex notation per default (used only by tex term editor)

use BoxPp

- added arrow notation
- typo fixed ("Pi" vs "pi")

patched

inductive type ident optional in mutcase

added regtest for optional inductive type on mutcase

s/pcre/str/

new (box based) pretty printer

split configure.ac in two parts: ocaml and gTopLevel

added sample configuration file

- added support for variable interpolation
- switched from Pcre to Str for regexps :-(

patched for *.cmx

new .depend files

removed some anciente debugging messages

libraries-complete.ps:
 * square nodes now have a yellow blackground
 * pxp-* packages collapsed to a single node pxp[-*]

libraries-complete.ps: the internal libraries are now all squares while
the external libraries are circles.

Added new target libraries-complete.ps (with also all the external
dependencies).

Example configuration committed.

Ported to Http_registry and to HelmLogger.

getter's revolution (now uses backend in ocaml/getter)

Ported to Helm_registry.

bugfix: auto_disambiguation is not considered for searchPatternApply

- script.sh removed from CVS. script.sh.sample added isntead
- triciclo.conf.xml.sample added

fixed typo

new logger

new getter, logger, and the hell

new logger, getter, and the hell

support for subst

new metas (getter's backend, registry, logger, and the hell)

ported to new getter (backend)

ported to helm registry

ported to new logger

use debug_print in a debugging message

- getter revolution: split backend and frontend (this is the backend)
- working remote part but not yet the local one (extra unneeded headers)

- split away gtk logger
- renamed module to HelmLogger

added some debugging messages

A type checking error report now prints also the metasenv.

added target *.opt (e.g. test.opt, librarytest.opt, etc.)

- make *opt fixed
- added -vars -varsprefix cic:/Coq to testlibrary

Big changes:
  1. every level now catches the *Failure excecptions of the lower level
     and converts it to its own *Failure. The same for *Uncertain.
  2. CicMetaSubst.delift now raises also Uncertain (that is converted
     to CicUnification.Uncertain and then to CicRefine.Uncertain).