Typing of intros_tac improved. It now has a parameter that is a fresh-names
generator.

Quick implementation of the "inst" csymbol. It can surely be improved.

First working version of the possibility to introduce new inductive type
definitions. Many checks have not been implemented yet and the interface
allows you to progress to further stages even if the input is incorrect.
Nevertheless, if the input is correct it will be accepted by the kernel,
saved to disk and notified to the getter.

This is the dawn of a new set implementation era.

put_inductive_definition implemented and exposed.
It is a very UNSAFE solution to the problem of computing inner-types of
non-debrujined mutual inductive types (whose constructors referes to
the not-yet-defined inductive type block): you can use this function to
add the block to the environment; then you compute the inner-types; and
finally you save the object and register it to the getter.

typecheck_mutual_inductive_defs exposed.
It is used to type-check and inductive definition which has no URI associated
to it (i.e. it is not managed by the getter; e.g. when it is not saved yet
since we do not know if it is well-typed).

An exception was raised when a MutInd or MutConstruct had an uri to a
non-existing object. The whole URI + XPointer is now printed.

Added new tactics: Exists, Split, Assumption, Absurd, Generalize (doesn't work)
Moved ElimType from ring.ml to variousTactics.ml
Moved Contradiction from fourierR.ml to variousTactics.ml

m:exist ==> m:exists

First implementation of the new generalized SearchPattern on the whole
type (not only the conclusion). Despite the file name, no levels have
been implemented so far.

Brand new implementation based on functors taking a strategy in input.
Several different strategies have been implemented. Unfortunately many
of them are incomparable and there are critical examples where only some
of them terminate in reasonable time.

Removing the functor/module stuff does not bring any sensible performance
improvement even for simple strategies (where most of the functions are
just identity fuctions that can be inlined when not crossing functor
boundaries).

- added a level of quoting on xmluri parameter because libxslt's
  document() implementation sucks

*** empty log message ***

- now esempi/fourier/ is he dir for all fourier extras
  - fourier.cic some tests
  - fourier_benchmarks.cic some test computionally interesting
  - fourier_make_benchmarks.ml a simple tool to generate big systems of
    inequations

Now MQueryGenerator generates the query and MQueryLevels produces the restrictions (must and can).

bug in hypotesis parsing solved

* iff notation added (new csymbol)
* New notation for lists added (list.xml)

lazily ==> call_by_name (since it is really a call_by_name!)

The default is now false (i.e. call_by_value strategy) to make an example
of Fourier application type-check in 8s instead of 1h40m!!!

We also tried a call_by_need strategy (not committed).
The results obtained are so far equivalent to the call_by_value strategy
(that is why we did not commit the code).

patched Makefile to link also ../gTopLevel/mQueryLevels.cm{o,x} which
were splitted away from ../gTopLevel/mQueryGenerator.cm{o,x}

Relation patched, property added.

* The new query language (now broken) works only on the new DB
   helm_mowgli_new_schema.
* InConclusion, InHypothesis and so on are now inserted in the DB with their
  namespace.

generator patched

comments in fourier.ml now are in ocamldoc style
bug in fourierR.ml (wrong Rel) solved

&CSCbr; replaced with 
 to make libxslt stop complaining.

New module for level management (was in MQueryGenerator)

Generator updated for new MathQL.ml
Level functions decoupled from Generator

Changed cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind definition

Now it is possible to define a 'cookable' operator with arity = 0 and  hide = 0

toplevel.ml patched but it doesn't compile with open and free variables.

- use 'query_of_text' to parse textual queries
- use 'helm_mowgli_new_schema' as database

- catch processing exception which are now reported embedded in html responses
- catch parameter exception which are now reported as bad request responses
- changed default port from 48085 to 58085
- disabled http debugging

- first (draft) version of searchEngine

WARNING!!!
From now on the V7_3_new_exportation branches of ocaml/mathql and
ocaml/mathql_interpreter are DEPRECATED!!! You must switch back to
the main branch.

Some stylesheets are now generated with Di Lena's meta_style.
Remember to add a new entry in servers.txt!!!

Porting to the new DTD for MoWGLI.

This commit was manufactured by cvs2svn to create branch
'V7_3_new_exportation'.

- removed: cut_tac False to demostrate False
- removed: apply_tac Rle_zero_zero
- a new big example

~ask_dtd_to_the_getter parameter added to Cic2Xml.print_innertypes

Param ~ask_dtd_to_the_getter added to Cic2Xml.print_object.

Big change: Qed saves the theorem/definition and registers it to the getter.

innertypesuri_of_uri implemented

Interface improvement (???): the Check button has been moved to a brand new
menu.

Small interface improvement: the menu is now in an handle_box (i.e. it is
detachable).

...

Interface improvement:
 * "State" button replaced with a menu item;
 * the URI is now requested to the user

Code clean-up: the widget in the lower-left corner is now a widget to input
CIC terms, featuring the following methods:
* get_term
* set_term  (issue: what should be its type? So far the input is a string)
* reset

Aliases definition removed from the CIC textual parser.

Aliases definition removed from the

Inteface improvement: the "Edit Aliases..." menu entry now opens a window where
aliases may be entered and modified. I am now going to remove aliases
declaration from the CIC textual parser.

Major interface improvements.
The aim is to substitute the GEdit widget to input text with a widget to
input Cic terms.

Rendering of InductiveDefinitions, Variables and Axioms implemented.

URLs_or_URIs param added to choose if the xlink:href should be an URL (i.e.
a request to UWOBO to ...) or simply an URI (i.e. cic:/...).

Identifier added to inductiveType in the DTD.

IllFormedUri exception now exported.

Order of the generated metavariables for apply fixed. Nothing seems to
break (a miracle?)

Comments improved.

Bug fixed: conjectures were printed in the wrong order.

Metasenv partially checked.

* Bug fixed: a real empty page is now really used for the empty notebook.
  The Not_found exception is no more raised.
* Small interface improvements.

Residual interface bug fixes: no sequent page is now forced twice.

Small interface improvement: the first goal page is no more forced unless
the current goal is the first one.

Open bug: the current goal is forced again when visited a second time!

Small interface improvements.

Other small improvements to the general window layout.

name fixes due to changes in libhttp-ocaml (e.g. s/Http\.Daemon/Http_daemon/)

Default for the reduction moved to CicReductionMachine.

Small interface improvement: selecting something in the proof does not
unload any more the current sequent.

Interface improvement:
 - the pages of every notebook are now generated with lazy code
 - the interface to choose between several interpretations is now really nice

Interface improvements: the window to disambiguate uris is now reasonable.

TODO: the stylesheets should be applied lazily for the pages of the notebook
 of the check window.

switched to OCaml HTTP module

Written instantiate for content level

A frame now surrounds the XMHTML widget.

symlink automagically cicReduction.ml if it doesn't exist

Heavy restyling of the interface.

Open BUG: exportation to PostScript sometimes make the widget core-dump.

An old bug in 'eqT' hipotesys solved

Modified mode "abstparam" due to changes to LAMBDA and PROD. To verify if there are errors.

- big interface changes: open goals are now collected in a notebook
- the code is less functional than before ;-(

Open bugs/features:
 - the notebook page is re-generated (and stylesheets are applied again)
   even if it was already full

mathql_interpreter_galax removed

Quick fix to view metadata theories again. The case were we are interested
also in bodies is not handled correctly yet.

nameObject ==> objectName

The reduction tactics are now shared between ReductionTactics and ProofEngine.

The fold tactic of proofEngine now uses ReductionTactics.fold_tac.
A parameter was added to choose if the reduction must be performed also
in the hypotheses.

- Comments updated
- Eq renamed to eqT

- synchronization with the main branch

- porting to the new theory with explicit named substitutions completed
- bug fixed: fold used to undo an over-simplification of RewriteSimpl

- new fold tactic

- new CicTextualParser
- improved disambiguation of parsed stuff
- improved interface for disambiguating uris

New CicTextualParser: it now returns (approximately) a couple
list of free names * function from an interpretation to a Cic term
where an interpretation is a function from string (ids) to uris.

Corrected some wrong paths

Corrected some wrong paths

Several bug-fixes:
 - URIs shortened
 - Assumption did not lift the hypothesis ==> the unification always failed

Bug fixed: the declared number of new goals of Apply was plainly wrong.

Better layout of the buttons.

Added variousTactic with Constructor, Left, Right, Exists, Reflexivity, Symmetry, Transitivity
Added tacticals Repeat, Do, Try, Solve

- ElimIntrosSimpl now implemented using tacticals. It becomes an
  ElimSimplIntros (which does lambda-abstraction with the reduced type ;-(((
  To be fixed.
- reductionTactics now also have the usual interface for tactics

explicit namd substitutions introduced

New euristich for the unification: convertible terms always unify.

Metadata DTD changed.

Porting to the new metadata DTD.

Undo of the previous commit (that was a mistake).

Bug fixed in reduction/simplification of explicit named substitution.

Dead code removal.