No more garbage in the metasenv.

New target librarytest (to apply testlibrary.opt to index.txt). The output
is in LOG.

- added support for multiple choices
- added pping of toplevel exceptions

better output format

flush stdout after print_string

debug prints on stderr

removed duplicated entry about freshNamesGenerator

- added testlibrary .opts
- build just gTopLevel per default

added \to notation for anonymous binders Pi and Lambda

bugfix: use rev_uniq also on non-located term

sort_of_prod relaxed to accept also Metas (when the second Meta has an
empty context). In this case the second Meta is returned.

- sort_of_prod now returns the second Meta (if it is a Meta) after
  unifying it with a fresh Meta whose context is empty
- the name generated by eat_prods where not always fresh. Fixed.

added html_of_html_msg

__n no longer generated.

"assert false" relaxed to a warning.
The problem raises when a non-dependent type is found and there IS a Rel
to it. It used to be an assert false (that failed). It is now relaxed
to a Cic.Anonymous (plus a warning on stderr).

No longer puts anonymous declarations in the canonical contexts during
eat_prods.

- the result of a refinement is now cleared from dummy dependent types
  and letins
- freshNameGenerator: bug fixed

freshNameGenerator.ml* added

rebuilt

added freshNameGenerator

added testlibrary script

use a dummy location when no location is provided

added ( ) notation for binders

dummy dependent types and dummy letins are now removed from the refined
term.

fresh_name_generator has now also the metasenv parameter.
Before this patch it used the empty metasenv (and it worked, somehow!)

mk_fresh_name moved to FreshNamesGenerator.

New test.

Final answer: the local context MUST be normalized w.r.t. the canonical
context before delifting w.r.t. it. Reason: we normalize it only lazily and
this is a right place to ``force'' the normalization.

Restrict reimplemented to avoid generating lists of indexes to be restricted
that fall outside the context. It doesn't change much, really.

Added a TODO (to catch only the right exceptions instead of everything).

Bug fixed: the canonical contexts were traversed in the wrong direction
during restriction. As a consequence, some hypothesis were not correctly
restricted.

Rel to hidden hypotheses are now printed as _hidden_n.

ppterm_in_context exported

ppcontext (and thus also ppmetasenv) were buggy: the occurrences of a variable
bound to a previous entry were of the form -n (instead of showing the binder)

Functors must be applied using parentheses around the argument in OCaml.
CamlP4 accepts a looser syntax ;-(

Added newline.

Bug fixed: restriction of already restricted contexts was bugged (due to
a missing "incr i").

Effects of fixing bugs for other regression tests ;-)

We no longer apply the subst to a Meta in force_does_not_occur. In this
way we can restrict if something goes wrong.

delift no longer apply the substitution when a Meta is found.
Reason: in this way I can restrict if something goes wrong.

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