eat_prods reimplemented to generalize the output type of the application
a bit more (when it is a metavariable).

Added an optional parameter to identity_relocation_list. The parameter
is the "starting" rel.

More debug informations.

Substitution no longer returned from CicRefine.type_of_aux

ported to new type_of prototype

uses CicMetaSubst.ppterm where needed

- refine's type_of no longer return a substitution

ported to latest Ast changes (mainly capture_variable addition)

- added entries for capture variables parsing
- factorized function for parsing Cic.names

- added capture_variable entry and Cic.names here and there

- 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