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).

Added copyright notice.

Explicit Named Substitutions now supported.

CicCache ==> CicEnvironment (in testlibrary.ml)

- fixed final log reporting (that was broken by one of the previous commits)
- CicCache ==> CicEnvironment

Bug fixed: when an axiom was asked, an exception was raised (since the
check for an existent body was skipped).

patched

Only applications whose head was a constant were eta-fixed.
Result: sometimes the generated term was no longer well-typed.
The fix consists in calling the type-checker on the head of the
applications. Slower, but more reliable.

Bug fixed: checking inductive type declarations with left parameters (e.g.
le) lead to mistakes due to debrujin/undebrujin: terms to be debrujined must
be closed and then left parameters can not be removed _before_ calling
debrujin_constructor.

added "'" as a valid (continuation) identifier character

Added flag ?eta_fix:bool to acic_object_of_cic_object.

added thread entry

added netstring and pxp deps

helm-thread's META

thread library (actually contains just ThreadSafe module)

- added environment variable overriding
- XML syntax for configuration file

sort_of_prod now thinks that a "sort metavariable" is a metavariable where
no free variable occurs in the local context. Reason: there used to be a bug
induced by the fact that a metavariable ?1 with an empty canonical context
could be istantiated with a metavariable ?2[l] where l has no free variables
but still it is not of length 0.

Added is_closed.

split into two major parts:
- backend (ocaml API)
- frontend (web service)

bumped version (tag soon)

no longer use marshalled table for unicode macros

use CicAstPp

eat_prods now uses mk_implicit_type.

- Added mk_implicit_sort.
- Used in CicRefine.sort_of_prod.

Added mk_implicit_sort.

A better (but yet not empty) metasenv is now returned.

sort_of_prod: the second term, when it is a meta, was unified with a fresh
meta in a wrong context. Fixed.

- added options "-vars" and "-varsprefix"
- ported testlibrary to Arg module

changed deps since testlibrary now uses (minimally) BatchParser

rebuilt

sort metavariables are now generated in an empty canonical context.

added annotations to Cic.Implicit

use ledit for debugging