getter's revolution (now uses backend in ocaml/getter)

Ported to Helm_registry.

bugfix: auto_disambiguation is not considered for searchPatternApply

- script.sh removed from CVS. script.sh.sample added isntead
- triciclo.conf.xml.sample added

fixed typo

new logger

new getter, logger, and the hell

new logger, getter, and the hell

support for subst

new metas (getter's backend, registry, logger, and the hell)

ported to new getter (backend)

ported to helm registry

ported to new logger

use debug_print in a debugging message

- getter revolution: split backend and frontend (this is the backend)
- working remote part but not yet the local one (extra unneeded headers)

- split away gtk logger
- renamed module to HelmLogger

added some debugging messages

A type checking error report now prints also the metasenv.

added target *.opt (e.g. test.opt, librarytest.opt, etc.)

- make *opt fixed
- added -vars -varsprefix cic:/Coq to testlibrary

Big changes:
  1. every level now catches the *Failure excecptions of the lower level
     and converts it to its own *Failure. The same for *Uncertain.
  2. CicMetaSubst.delift now raises also Uncertain (that is converted
     to CicUnification.Uncertain and then to CicRefine.Uncertain).

Added copyright notice.

Explicit Named Substitutions now supported.

CicCache ==> CicEnvironment (in testlibrary.ml)

- fixed final log reporting (that was broken by one of the previous commits)
- CicCache ==> CicEnvironment

Bug fixed: when an axiom was asked, an exception was raised (since the
check for an existent body was skipped).

patched

Only applications whose head was a constant were eta-fixed.
Result: sometimes the generated term was no longer well-typed.
The fix consists in calling the type-checker on the head of the
applications. Slower, but more reliable.

Bug fixed: checking inductive type declarations with left parameters (e.g.
le) lead to mistakes due to debrujin/undebrujin: terms to be debrujined must
be closed and then left parameters can not be removed _before_ calling
debrujin_constructor.

added "'" as a valid (continuation) identifier character

Added flag ?eta_fix:bool to acic_object_of_cic_object.

added thread entry

added netstring and pxp deps

helm-thread's META

thread library (actually contains just ThreadSafe module)

- added environment variable overriding
- XML syntax for configuration file

sort_of_prod now thinks that a "sort metavariable" is a metavariable where
no free variable occurs in the local context. Reason: there used to be a bug
induced by the fact that a metavariable ?1 with an empty canonical context
could be istantiated with a metavariable ?2[l] where l has no free variables
but still it is not of length 0.

Added is_closed.

split into two major parts:
- backend (ocaml API)
- frontend (web service)

bumped version (tag soon)

no longer use marshalled table for unicode macros

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.