ported debian stuff to ocaml 3.08

The type substitution has been moved into Cic.

Subst has been added to the kernel.

* split evil let definition (ic, oc) = ... into two subsequent
  definitions
* using Gzip.open_in_chan to avoid file descriptor leak

Modified filtering function

cleanURI now removes also the part that follows the '#' symbol.

The URI passed to the control frame must be clean (i.e. no #xxx part).

The part after # must be removed for the control frame.

Bug fixed: beta_expand did not perform any recursion over the local context
of a metavariable ==> the local context was not lifted.

commeted out some debugging instructions

commented out some debugging instructions

Bug fixed: eta_expand did not perform any recursion over the local context
of a metavariable ==> the local context was not lifted.

Bug fixed: the beta_expansion function did not lift the argument before
attempting to match it ==> no matching was done correctly under an
abstraction.

...

New handling of substitution:
- splitted metasenv from substitution
- substitution enriched with canonical context information for
  checking_metasenv_consistency

added (commented) benchmarking code for the disambiguation paper

removed a useless test on explicit substitutions on variables with body

use get_obj to retrieve cic objects instead of typecheck

fixed typo

- new implementation of the apply case in fo_unif using beta expansion
- infinite loop fix while unifying terms in an invalid metasenv

ugliness changes:
- more google like look and feel for query results
- exceptions are no longer rendered in <h1> elements but pretty printed
  inside the standard moogle HTML template
- advanced search status is now rememberd between searches
- added results count
- added result type feedback in results page

Corrections to "auto" tactic

elim_tac rewritten almost entirely. It is now based on refinement +
one invocation of the (now more powerful than before) apply_tac.

Added new function compare_metasenvs.

Comments changed.

- In the case (?i args) vs term the term is now eta-expanded w.r.t. args.
  This allows to easily implement elim using apply and it makes the auto
  tactic much more powerful.
- CicMetaSubst.apply_subst semantics changed: it now always performs
  beta-reduction when a meta in head-position in an application is istantiated
  with a lambda-abstraction.
- CicMetaSubst.apply_subst_reducing no longer in use: removed.

New syntax.

Fourier URIs changed in V8.

- moogle replaces the old search engine

bugfix: ignore proof checker output

atmost/atleast/exactly constraints are now used only for the "hint" method.
They are no longer used for "match" and "elim".

in the particular case of simple searches, Andrea atmost/atleast/exactly
technique is used

first moogle commit

search.xsl added.

Added search.xsl (S).

Stylesheet whose input is an empty document. It calls the
new search engine (moowgle) passing the needed parameters.

New profile param: searchengineURL

Uncommited changes committed.

Interface URL can now be setted using the control panel.

Interface URL can now be setted.

The normalization of URIs when the DB is empty (or it is being filled) is
not reliable. As a consequence the semantics of the Http_getter_map has been
changed again: the only method that normalized the URIs before using them
is the resolve method. The methods replace, add, remove, etc. no longer
normalize their argument.

- new stylesheets in the predefined set
- some fields are now password fields

New attributes for ht:* elements proposed by Nijmegen.
All the attributes are IMPLIED and the default value for all of them
is backward compatible.

Objects ordering is now case-insensite.

fix for proofEngineTypes.mli

new universes implementation

Ordering is now done in no-case style.

theory:path/index.theory are not rewritten to theory:/path.theory
if theory:path/index.theory exists in the database.

New filtering function for "Auto" tactic using "just costraints"

Back compatibility code introduced:
 1. the ls method maps a theory theory:/path/filename.theory
    to theory:/path/filename/index.theory iff there exists at least
    one object of the form cic:/path/filename/*
 2. the getter handles every URI theory:/path/filename/index.theory as
    the normalized URI theory:/path/filename.theory

The theory index.theory, if present, is shown at the beginning of the
listing.

* makeProofTreeURL ported to the new interface

.body removed from bread crumb trail

Links in the control frame when the URI ends with .body are now handled
correctly (i.e. the .body is removed if meaningless, as for the proof-checker
or the metadata).

<xsl:import href="toplevel_header.xsl"/>
moved here from show_dc.xsl

<h1> ==> <h3>

stylesheet L added to the metadata chain

bread crumb trail added

metadataLib.xsl merged into metadataControl.xsl

Dead code removed.

defaults.js no longer in use

Files control.js graphLinks.js utils.js no longer in use.

Dead code inclusion removed.

No longer in use.

No longer in use.

ls2html.xsl no longer in use

Form to choose the number of nodes to show removed ;-(

&2C ==> %2C

Dead code removed.

New HELM interface almost stable.

* it is now possible to set multiple parameters upon creation (or cloning)
  of a new profile

* setpassword passwords swapped

* implemented setparams method for setting multiple parameters at once

...

param.processorURL added (need by the search engine)

target="_top" added to Search.

Link to the search-engine hard-coded.

Major interface upgrade still going on. But we are approaching the end of the
tunnel.

New icons.

Major interface upgrade still going on. But we are approaching the end of
the tunnel.

Bug fixed: ls?baseuri=(cic|theory):/a/ also returned theory:/a.theory.

* getparams returns annotated pairs key,values

bugfix in /ls: removed double trailing "/"

ported to regexp based /ls method

changed /ls method so that regular expressions are used instead of plain
URIs

Major interface improvements.

* bumped to new version

* added external documentation in tex format
* true=>public and false=>private for permissions

JSMmenu links fixed.

###############################################################
### Partial major upgrade of the HELM/MoWGLI Web interface. ###
###############################################################

WARNING: requires the new UWOBO profiles.

Known bugs:

 1. the JSMmenu for graphs is broken
 2. the configuration stuff is utterly broken: you should rely on
    the default configuration
 3. only HTML has been tested (MathML and ProofTrees are broken for
    sure)
 4. dead code everywhere (e.g. almost all the existent
    javascript code; several tokens in links_library.xsl)

New: UWOBO profiles added.

written a new sort function to postpone the resolution of some types of the goals

don't remove documentation on "make dist" so that documentation will be
part of the generated tarball

* setprofileparam ==> setparam
* serialization/deserialization of the profile file implemented (write-through
  semantics)
* cloning of a profile fixed

added hostname resolution entry

implemented hostname resolution for "addr" parameter

rewritten "start" comment, now is almost decent

emptied implementing all items

removed spurious messages

- ported to latest API
- bumped copyright info