1. folded maction are now selectable
2. metavariable occurrences are now displayed together with their
   substitution (to be improved)
3. the hypothesis in the metasenv are now displayed in the right order

* mime type updated

- support for comments added in mathql_db_map.txt

Unuseful id removed from hypothesis.

- information about the database map added in whatsnew.html
- spell checked

Eta fixing for MTCases added (that meant to recursively pass around the
context).

All the ids are now generated by gen_id. (Some of them were previously based
on the acic ids).

* quite a lot of patches in the building stuff

new links added

Added method FalseInd

Added method "FalseInd".

Prefixes introduced for the generated ids/xrefs. Example:
 "proof:" for proofs
 "decl:"  for declarations
 ...

- the mathql interpreter is not helm-dependent any more
- fixed a bug in the "match conclusion" query of the search engine
- gTopLevel/Makefile improved

Spurious files removed.

"(" moved from Mtext to Mo. Spaces removed.

Added method AndInd.

Added Method "exists".

Few modif in eta-fixing.

Missing xref for conjectures.

mathvariant=normal for all the proof ;-)

background (deprecated) ==> mathbackground

Bug fixed: it could have happened that the tree structured becomes scrambled
by the highlighting operation.

use OCAMLFIND variable instead of "ocamlfind" directly

- severe bug fixing
- implementation of two functions to highlight/dim set of nodes given
  their xref. [used to highlight/dim the current goal]

Highlighting of changed parts.

URIs of inductive types and constructors fixed.

Lemma generated wrong URIs (again). Fixed.

Complete beta reduction added to avoid strange case of deep beta-redexes
in the expected types of application heads.

Exact handled in a better way (no more "NO PROOFS").

The name of TD proofs was erroneously always set to previous.

Improved management of conclusions, to avoid repetitions.
Some problems of xrefs have been fixed.

- better handling of proof expansion/contraction
- helm:xref added in most places

- Lemma added to the list of proof arguments
- Lemma used for Const, MutConst and Var in Apply arguments
- atomization of complex proofs is now performed also in tactics different
  from Apply

Debugging stuff changed.

"Final" commit that patches termViewer while still enabling XML Diffing.
Awesome performances!

- selection attribute of maction is now explicitly generated
- all the conjectures are now put in a table to avoid too many
  changes that make Xml Diffing difficult.

Previous commit was erroneous and dit not compile.
Fixed.

Debugging code inserted bug in the code ;-)

XmlDiff-ing of DOM trees implemented.
SPECIAL FEATURE: the selection attribute of mactions are not patched.

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.