Added a new example.

...

report files are now produced (and removed) during regression testing

Patch to delift withdrawn.
The patch was used to nullify items in the local context when they where

...

Typo fixed. Used to break target gentest.

Bug fixed: when a variable not instantiated yet was restricted, some
nececssary restrictions were not performed due to a typo.

Improved regression testing reporting.

- regtest: better argument handling (using Arg)
- regtest: -dump and -nodump to dump the environment (that is authomatically
  restored if found)
- Makefile: new target envtest that generates the environments without
  changing the .test files

removed a debugging message

- improved some error messages
- sort_of_prod: returned argument wasn't lifted correctly, as a temporary
  patch return Type

moved here CicAst and pretty printer

ported to CicAst

- sorted domain which hopefully avoids exponential explosion
- ported to CicAst

moved Ast in cic_transformations/

- added support for implicit in concrete syntax
- ported to new Ast

regression tests

cic_mkimplicit' removed (its implementation was wrong and the function is
not really used)

Debugging code removed.

sort_of_prod changed to not generate a new metavariable in the case Meta vs
Sort. Reason: the new metavariable is not constrained in any way and, at the
end, we find it in the final metasenv.

- comment inside .test file that explain what follows
- use a list to clear buffers
- better comment for .test file format

added cleantest target (removes tests/*.test)

Check missed: the two metasenv were not compared.

Debuggin infos removed.

- do not crash any longer if type-checking or reduction fails
- prints also the metasenv

time added to regtest

catch just AssertFailure instead of _ (AssertFailure is the only
exception that could be raised there since the invoked function wraps
every exception inside it)

removed SortExpectedMetaFound special exception

added urimanager dependency

Meta vs same Meta now tries unification when convertibility of the two
substitutions fails.

s/LocatedTerm/AnnotatedTerm + various annotations/

New tests for lambdas (that show bugs in applications ;-)

catch exceptions and mark corresponding tests as failed

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*