use CicAstPp

eat_prods now uses mk_implicit_type.

- Added mk_implicit_sort.
- Used in CicRefine.sort_of_prod.

Added mk_implicit_sort.

A better (but yet not empty) metasenv is now returned.

sort_of_prod: the second term, when it is a meta, was unified with a fresh
meta in a wrong context. Fixed.

- added options "-vars" and "-varsprefix"
- ported testlibrary to Arg module

changed deps since testlibrary now uses (minimally) BatchParser

rebuilt

sort metavariables are now generated in an empty canonical context.

added annotations to Cic.Implicit

use ledit for debugging

Comments (notes) removed.

Code riorganization.

added Format-library-friendly pretty printers defined on top of the
previous ones (still exported)

added -g flag to ocamlc per default

textual term editor is now the default one

ignore .debug_script (used by Makefile's debug target)

- split regtest/testlibrary/gTopLevel objects so that the first two
  aren't linked in thread mode
- added debug target to debug with wowcamldebug executables
- link with -g per default in bytecode mode

Bug MutCase fixed: now the type of the constructor only eats the
left params.

added testlibrary.opt and some cm****

NameExpected exception removed. The "identifier" __n is now returned
(as CicPp does).

Improved error messages.

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