functor added

patched and improved

first version

This commit was manufactured by cvs2svn to create branch
'unlabeled-1.4.2'.

- 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.

- 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