- changed ast for pattern matching so that type annotations are possible
- bugfix for indexes in Fix/CoFix cases

- big hack: keep on unifying/refining when SortExpectedMetaFound
  exception is encountered

- removed metasenv argument from kernel proxies invocations
- lift_meta over defs with an explicit type implemented
- reimplemented eat_prods (open bug: when an application has more than
  one argument and its type is a meta then the outtype is a Meta whose
  context is not general enough. To be implemented)

- added SortExpectedMetaFound exception (huge hack)
- more information along with assertion failed "9"

- bugfix for expand_implicits, return correct term on Fix and CoFix cases

- removed unwind: every substitution is now _not_ unwinded
- removed extra metasenv argument from all kernel proxies
- added kernel proxy: subst (for CicSubstitution.subst)
- added pretty printer ppterm

changed prototype of CicMetaSubst.apply_subst*

added comments

fact regtest

reordered

added string_of_html_msg

- typo bugfix: INT token no longer exists
- use "=" instead of \def for let definitions
- added a new "binder" level so that \forall n. n=n binds correctly

Refinement of Fix and CoFix now implemented.

- removed ancient refine exception
- s/Try every selection/Try selected/ on a button

added regression tests

s/Callbacks/DisambiguateCallbacks/

- lift added to CicMetaSubst
- refine of Fix and CoFix implemented
- bug fixed in refine of Cast

- s/TexTermEditor/TermEditor/ (* former no longer appropriate)
- added "auto disambiguation" setting support

- added "clear alias" menu item
- added "clear" button to the "edit aliases" window

- occur check test anticipated to the delift phase
- uses CicUtil.lookup_meta

use CicUtil.lookup_meta

bad link patched

s/List.find.../CicUtil.lookup_meta/

added CicUtil module with just lookup_meta function

empty goal patched

opt goal fixed

test for empty string given, if so return Environment.empty without invoking the parser

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.