1. Modificiations due to the change ot K.Aux
2. Assert false on Lambda with no name removed. Who generates them?

The Aux argument of conclude is now of type string (used to be int).
Case Fixed.

Interface change: only cobj2obj is exposed.

Flattening application contexts uncorrectly changed the proof ids.

** UNTESTED **
Fix and CoFix are now handled "correctly" ;-)

We do not compute inner-types for the metasenv ==> we handle it in a particular
way, always generating `Declaration and `Definition (instead of `Hypothesis and
`Proof when the sort is Prop).

Rendering of current proofs completed.

Reindenting.

proof2cic now uses Deannotate.deannoate_term instead of having an input
parameter.

Cic2acic is now responsible of eta-fixing the objects.

Cic2acic is now responsible of eta-fixing the objects (using the Eta_fix
module).

cic2content.ml* moved from cic_transformations to cic_omdoc.

Content2cic e Eta_fixing moved from gTopLevel to cic_omdoc.

...

cic_transformations factorized into cic_omdoc and cic_transformations.

Cic2content split into Content and Cic2content.

CSC: tentative definition of the ocaml structure that represents
 OMDoc objects.

some documentation added

Partional first fase final.

dead code removed

Persist file completed.

- new generated query "unreferred" implemented at server side
- fixed some aspects of the constraint generator for "matchConclusion"
- fixed a bug that prevented to "make opt" in ocaml/gTopLevel

* changed name of shared library

* snapshot

* added simple test program

* the container seems to work now

Xml.token is now namespace-aware. As a consequence, xml2Gdomexmath is
no longer needed. (It was a terrible hack indeed).

Control Factory modified.

persist file with factory.

Several changes (the beginning of a new era???)
 1. stuff related to transformations (stylesheets and so on)
    moved from gTopLevel to the new library cic_transformations
 2. porting of the stylesheets to old plain ocaml code by Andrea Asperti.
    Also in cic_transformations.

Disclaimer:
 A. the ocaml transformations are still incomplete and under development.
    They are a bit more performant, though. (just a few order of magnitudes)
 B. the cic_transformation library seems a bit of a mess right now.
    Much clean-up needed.

added persit-file-implementation.

* changed name to control factory

* updated the help file to reflect the new syntax (reload/remove)

* syntax update for "remove all stylesheets" in control.js
* reloadAll function created

* added .pc file
* IDL interface version computed from package version

Camera ready.

* substituting the right version variable

* wrong variable for version

* patched version of shared library

* first snapshot

merged CSC's typos squashing

fixed "s" typos

description for "Irene Schena" added in authors.html

wrapped libxslt stylesheet application inside an ocaml blocking section
so that ocaml exceptions, signals and other asynchronous stuff could be
handled in the meantime

bumped version to 0.0.5

Towards the camera ready.

debian release 0.0.4-7

debian release 0.4.3-3

reordered link order

Version dumped.

Bug fixed: the value of parameters must be valid XPath string literals ==>
they can not contain both ' and " (at least in Veillard interpretation, of
course ;-)

The fix applied consist in accepting parameters with only ' or only " inside
by quoting them using the opposite quote. As a consequence, variable
values with just 's inside are now handled correctly.

prose patched

links page added

implementation and whatsnew pages added

"backPointer" metadata enabled

new "light" implementation of intersection (compatible with the generator)

rendering of "meet" patched

Bug fixed: deselecting a constraint just forgot its depth.

mathql_generator: new constraint format (more type safe)
mathql_test     : moved outside ocaml

Ctr+Backspace is now enabled. Used to perform "alternative" deletion.

The editor window now scrolls when the user exceeds the available space.

- DoubleTypeInference.does_not_occur exposed
- dummy bindings in Prods are no longer generated: arrows are now generated

- changed changelog author to me (to GPG sign the package)
- added dependencies on gmetadom >= 0.1.10-2 (so that the .pc is available)

0.4.3-2

1. freeze/thaw added to reduce flickering due to selection changes
2. SEMANTICA CHANGE: structural selection is no longer activated just
   before semantic selection

gtkmathview-config and gdome-config no longer used

debian release 0.0.4-6

moved debhelper compatibility level to debian/compat

- default font size of the proof window lowered to 10
- the font size spinner is now initialized with the right value

mathql_interpreter: natile-galax package removed from Makefie and META
mathql_generator  : MQueryLevels2.ml patched (namespaces removed from sorts)

The type of a LetIn is now a LetIn if and only if the bound variable really
occurs.

The "Save proof" menu item is now activated when a finished proof is reopened.

Reindentation.

Reloading bugged stylesheets no longer makes gTopLevel crash.

Reload stylesheets menu entry added (under the Settings menu)

...

http://....#Prop shortened to Prop due to a bug (feature?) in the DB.

relativeDepth function removed (useful only for cooking)

Metadata tools are now working correctly also over .body files.

The proof-checker should now be working also on .body files.

dropBodySuffix function added

- Object URL link added
- rethorical text changed

Ported to the latest version of libhttp

added tons of #include <cassert> to make latest gcc compiler happy

preliminar 0.0.3-2 debian release

forward ported to use pkg-config

It should have already been moved to ocaml/mathql_generator

Removed (it should have already been in ocaml/tactics)

Porting to the latest version of PXP (1.1.94).

No longer in use.

Branch V7_3_new_exportation merged.

Branch V7_3_new_exportation merged.

- help method added
- branch V7_3_new_exportation merged

styles directory creation now works even if stylesheets and meta_stylesheets
are symbolic links (as in my case)

Author specification added in head comments;
MQueryGenerator.builtin ready to be used

...

Installation instructions.

- script.sh added to the repository: you should change it to reflect your
  own settings
- the Makefile tries now to automatically build the styles directory, made
  only of hyperlinks to the styles in stylesheets and stylesheets/generated.
  Before doing make, you have to check out the stylesheets and meta_stylesheets
  repositories from the mowgli archive.
- added rootcontent.xsl which is the version used by gTopLevel until we find
  a better solution. You should change it to reflect your own settings.

New version 0.0.3:
 - tml-litex.xsl was not installed
 - guiGTK.h did not include gdome.h
 - configure.ac was not correctly ported to pkg-config, since it still
   checked for the existence of the *-config executables for all the
   packages editex depends on. Fixed.

* mquery_interpreter logging and debugging activated
* bug fixed: the universe of the complete search pattern must exclude
  the InBody occurrences