Computed inner-types are now also put in whd normal form.
This is at the same type too strong (e.g. it performs delta-reductions)
and too weak (it is not full-reduction).
We can consider this just a patch waiting for Coscoy's double-inference
algorithm implementation.

Bug fixed: the unwinding was not recursively performed. (a "t" should have been
a "t'")

META parsing was completely broken. Fixed.

gdome_xslt ==> gdome2-xslt

...

* Many improvements (expecially in exceptions handling)
* The cases in which existential variables are now handled "correctly"
  have been increased. Neverthless, existential variables are still implemented
  in a completely wrong way.
* First commit after the commit of cic_unification.

Old and dead code from the previous implementation removed.

First (very bugged) version of cic_unification committed.

Bug fixed in type_of_aux (Cast case).

Grammar factorized to avoid shift/reduced conflicts that were handled in
the wrong way. No more conflicts left.

'-' no more allowed in identifiers

* New implementation of Apply and Elim based on the latest implementation
  of the unification (not yet commited)

Modified Files:
1) grammar.txt: changes
Added Files:
1) query.xml: query example
2) xmathql.dtd: dtd for mathql

Modified Files:
1) grammar.txt: added new entries.

* The interface of CicTypeChecker now allows the usage of definitions in
  contexts.
* Let...In tactic implemented (but not tested!)

* env renamed to context everywhere in cicTypeChecker.ml
* Definitions should be allowed in the contexts as well as Declarations.
  This is the very first step: the notion of context is introduced in cic.ml
  and the interface of cicTypeChecker.mli reflects that. (Of course, also the
  interface of cicReduction should do the same!)
  The new implementation just raises an exception when a definition is found
  in the context.

Added Files:
1) grammar.txt: grammar of the Mathematical Query Language

Bug fixed: reduction in the scratch window now works even if there is no
proof in progress.

Reduction tactics in the scratch window implemented.
NOTE: if you select an hypothesis and you apply a reduction tactic, nothing
 will happen and no error message will be reported!

Debugging stuff removed.

Scratch window is now also raised (= hide + show ;-| when updated.

* Error reporting improved
* Check now also works when no current goal and/or no current proof is
  available.

* Scratch window added
* Check command implemented

Modified Files:
1) arith.xsl: ci -> cn for O

* Many improvements
* The interface now gives the user the possibility of (re-)opening an existing
  constant.
* Tactic Elim no more exposed in the user interface. Replaced by ElimIntros.
* Selection of subterms in the hypothesis of the goal is now "sound".
* Reduction tactics (Whd, Reduce, Simpl) now work also on the hypothesis.
  New bug/feature: their changes are lost when moving to another goal
  and coming back afterwards.

Module Logger added.

type_of_aux' (to get the type of a term in a given environment and context)
exported

pp exported

Ooops. Comments in .mly must be delimited by /* and */

* identifiers can now also have digits in them
* arrow notation for non-dependent Pi-abstraction introduced.
  It seems to be bugged w.r.t. application (a problem of priority?)
* CicTextualParserContext provides an highly not-reentrant implementation
  of parsing in a given environment

* Many improvements
* Added the possibility to select parts of the goal of a sequent and retrieve
  the corresponding CIC term.
* New tactics implemented: Cut, Whd, Reduce, Simpl, Change

Added the possibility to select parts of the goal of a sequent and retrieve
the corresponding CIC term.

Removed the patch to avoid a bug of gmetadom.

...

proofEngineReduction.ml added
It holds functions to perform reduction and simplification of terms.
They are used in the implementation of the reduction/conversion tactics.

* Bug fixed: applications of MutCase that are not iota-redexes were reduced
  just to their head.
* More debugging enabled (to be removed when code becomes stable)

Invariant enforced: no Appl of another Appl.

1. CicReduction moved into CicReductionNaif
2. CicReductionMachine is the new implementation based on an
   "environment machine".
You must make a sumbolic link from one implementation (.ml) to
cicReduction.ml

Replaced with a symbolic link to the actual implementation.
The symbolic link must be created after check-out.

type_of_aux' exported.

Meta implemented.

Modified Files:
1) mmlnotation.xsl xslt_index.txt: MathML default presentation now is
   generated by mmlctop.xsl
Added Files:
1) mmlctop.xsl mmlctop2_0.xsl: link and new Igor stylesheet for MathML default
   presentation

* New slides from Saarbrucken
* DTD changed

added debian stuff and a makefile with "dist" target

changed name to gdome2-xslt

- added -fPIC when creating .so
- added PREFIX variable support

changed package name to gdome2-xslt

cma names parameterized in configure @PACKAGE@ variable

-7 debian release, hopefully build also on HPPA

added -fPIC option when compiling ml_gtk_mathview.o

New data.

First MOWGLI paper. Many others will follow.

The first MOWGLI paper. Many many others will follow.

During the computation of the inner-type of a LAMBDA, the grandfather
was retrieved instead of the father. Fixed.

* Many improvements
* Proofs are now rendered in natural language. The inner-types file is
  store in /public/sacerdot/innertypes and directly retrieved from there.
  We must find a better solution.
* Apply tactic now implemented. It is based on the unification stuff of
  Andrea.

Declaration and Definition renamed to Decl and Def because
Definition was already defined in the DTD.

Sequent rendering improved: "=======" replaced by a single solid line

1) Sequent object added.
2) Current Proof and META rendering improved.

* Many improvements.
* Intros and Exact are now implemented.
* Inner sorts are now generated and used.
* Perforation of the proof is now implemented.

First commit of our future proof-assistant/proof-improver (???)
This commit is based on some un-committed changes to our libraries. So,
it won't compile out-of-the-box.

Added Build-Depends on t1lib-dev

Added build-depend on libgdome2-cpp-smart-dev.

- added some .mli and .ml to the debian package
- added depends on libgdome2-ocaml

preparing for 0.1.4

added libxml/ in #includes (see libxml2 ChangeLog)

error in check for xml2-config

gMathView.mli added

Electra forms added.

The contract is now on-line (but for an excel file still missing).

- Increased debian version to 0.3.0-3
- Added build depends to latest gmetadom and gtkmathview

The compilation of the test is restored.
It didn't compile any more due to a different behaviour of gcc on woody.

Links to the version with frames fixed.

Rendering improved.

Rendering improved.

New MOWGLI member.

New data.

Layout improved.

frames/no frame switch changed

Links between the versions with and without frames.

New data.

mowgli-adm mailing list created

New MOWGLI member.

* New data
* New members

New data.

MOWGLI roles considered in people position

* New MOWGLI members
* New: summary of the MOWGLI kick-off on-line

New data.

New: Minutes of the kick-off

People in the "by site" list are now sorted alphabetically.

* Some documents were not valid
* Project Leaders added to every package
* New data in project-management

* Work Package Leaders added (and rendered)
* Rendering of Work Packages improved

Added build dep on libgdome2-dev

Debian changes for version 0.3.0 of lablgtkmathview.
Major changes:
- split shared library package
- debian native package, diff.gz is no longer needed

The contract was the proposal!!!

Data refined.

Initial version.

* Linking was still static for native compilation.
* Automatic compilation of the test in native mode can no more be performed
  because the dynamic library is always searched in the position where
  it will be installed ;-(

Data refined.

More data.

New data.