snapshot (notably: first working version of the console)

- moved up in the grammar precedences command entry so that sequence of
  commands are not permitted
- added parsing of "abort" command

removed traliling dot in command pretty printer, now it's added by the
tactical pp

added Abort and Check commands

embedded commands ast into tacticals ast

- moved command as sub-entries of tactical grammars (as per tactics)

snapshot

- moved applyTransformation initialization code to the relevant library
- decoupled termViewer from ChosenTransformer

moved here initialization code (previously in gTopLevel/termViewer.ml)

snapshot

- added a configuration variable for selecting between fresh instances
  for numbers or not (set by default to a single instance)

snapshot

added a TODO comment

rebuilt

added extra "id" parameter for input_or_locate_uri callback

- split logic operators away from aritmetic ones so that
   \forall n:nat. n > 0 \or n = 0
  is parsed "correctly"

removed file:// prefix from local_library key, hopefully it isn't useful

snapshot

gt URL pointed to lt

Universes introduction

rdfly hardcoded URL changed from mowgli.cs.unibo.it to localhost

expandasking parameter passed to UWOBO.

snapshot

mysql_connection.* keys added

mathql_interpreter.mysql_connection.* keys added.

added (and used) some type shorthands

- added some type shorthands
- added license information

rebuit

Patches to generate ?1 : ?2 : Type in place of ?1 : Type removed.
It is interesting to understand whether it is still necessary (after
the CicUnification bug fix) or not.

Big bug fixed: in the case  t <?= ?1, the instantiation ?1 := t was generated
and then t : C and ?1 : E were retrieved/computed correctly; then
E <?= T was incorrectly tested (instead of T <?= E).

fourier.mli addedto interface files.

snapshot

added /help method (needed by respawner)

IMPLEMENTATION_FILES now generated from INTERFACE_FILES.

added .cvsignore

detects and uses {ocamlc,ocamlopt}.opt when available

detect and use {ocamlc,ocamlopt}.opt when they are available

exported term_of_uri

added helmLibraryObjects.mli mention

added .mli

got rid of a ~status label

got rid of ~status label

got rid of ~status label so that tactics can now be applied partially,
delta reduced, ...

added ocamlfind library checks to configure.ac

renamed mathita to matita

snapshot

ignore Makefile since now it's generated by configure

added Makefile.in

reorganized metas so that pxp is references only through helm-pxp

added hbugs' (client) meta

generalized META.* ignoring

- reordered modules so that pxp could be used as entry point for pxp
- added hbugs
- pretty printed modules

- use PxpHelmConf
- no longer use deprecated Pxp_yacc module

- use PxpHelmConf
- no longer use deprecated Pxp_yacc

use PxpHelmConf

added dep on Helm_registry

use PxpHelmConf module

- use PxpHelmConf
- removed references to deprecated Pxp_yacc module

- embedded ClientHTTP module (not very nice, but ClientHTTP shouldn't
  belongs to Getter module!)
- added PxpHelmConf module, repository of Pxp configurations for helm

added ExtThread module, ex Hbugs_deity (a Thread module with killing
capabilities)

injected hbugs under ocaml/ dir

moved hbugs under ocaml/

fixed a typo (inside a comment)

test_equality_only was not used in sort comparison.
It should be implemented only in unification.

use respawner

changed logging message

removed deprecated uwobo_forever.sh

removed tedious "_mowgli" postfix

use new daemon_respawner.sh

fixed some typos in sample init.d

added generic daemon respawner

script deprecated

added newline to log when log_file is in use

- addead autoconf-iguration. Actually it only set the default runtime
  configuration file

- use new logger interface
- added support for log_level and log_file in configuration file

- rewritten http_getter logger interface

- added sample usage of get_opt method
- added method get_opt_default (like get_opt with an additional default
  value)

Metasenv added as parameter to eta_fixing.

s/dtd_base_url/dtd_base_urls/

- better pretty printing of exceptions (added red color)
- added "-update" command line parameter for batch updating

- fixed dtd_base_urls implementation
- factorized a lot of code in document patching

- better pretty printing on /update
- added stdout logger

added string_of_html_tag (plain text pretty printer for tags)

added support for multiple dtd_base_urls

updating all sections

patched

Bug fixed: the following happened.
Auto generated two goals.
Closing the first goal instantiated also the second goal.
But we were still iterating over the original list of goals ==> BOOM!

added exists_meta

patched

updating the introduction

ported to latest polymorphic variant types

Added flag test_equality_only to are_convertible to better implement
the <=_{\beta\delta\iota\zeta} relation.

Added flag test_equality_only to are_convertible (to better implement
the <=_{\beta\delta\iota\zeta} relation).

added a missing <br> tag

implemented save_to

- uncommented save_to function (now implemented)
- added (tiny) description of the 'variable interpolation' feature

added Unix dependency (needed in order to run xmllint)

eta_fixing of the CurrentProof metasenv is wrong, since eta_fix does not have
the context parameter. Fixed by avoiding CurrentProof metasenv eta_fixing.

The parser accepts terms with metavariables as statements of theorems ==>
metavariable instantiation must be propagated also on the theorem statement.

- added test file