helm registry's META

helm registry --- first release

sample aliases language

Notation for Case revisited and completed.

Generated ml files added.

raise proper exception when a regexp fails on term_of_uri

don't remove METAs on clean, but on distclean

- s/id_to_uris/environment/
- bugfix: aliases work again

reference moved EnvironmentP3 for new parser

- factorized DisambiguateChoices module
- implemented alias language for gTopLevel

optionalizide some class parameters

.in version of "configuration" modules

debug_print

new configure.ac with support for compile time configuration of termeditor/parser/...

split a term0 rule for dinamycally change top-level (i.e. non-recursive) term rul

collapsed parens in a singol token

added tex notation

tex notation for compatibility with texTermEditor

- quiet debugging for mathql
- defined a debug_print function with a verbosity level

Eureka!
It is now possible to choose independently:

 - the widget for the term editor
 - the disambiguating parser, i.e.
   * the parsing component
   * the disambiguating component

ported to new module names

handle Cic.Anonymous

renamed modules so that they are more consistent with other cic modules

moved environmentP3 in cic_textual_parser2 and reshaped interface

implemented interface for gTopLevel

moved term_of_uri in cic/

moved here term_of_uri

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