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.

Minor interface improvement.

- (Partial) porting to the new theory with explicit named substitutions
- Porting to the new DTD
- Porting to the new query language and to its implementation
- searchPattern implemented: it performs an old "backward" query and then
  tries to apply every result to filter out false matches

Open bugs:
 - ElimIntrosSimpl, Fourier and Ring still to be ported
 - many, many, many others

Correct errors due to a different form of LAMBDA

Written particular uses of induction and corrected some wrong paths

Correct CurrentProof

Better implementation of the trusting machinery: some CicEnvironment functions
now have a trust optional attribute (that defaults to true). The TypeChecker
uses the false value only when type-checking the topmost object.

Every other operation of the kernel uses the true value (i.e. it trusts).
Is this really a safe behaviour? Hmmmmm. We need a proof here.

Merging of the modifications of Lorenzo on the main branch. They
implement the Fun constructor in a uniform way.

Correct CurrentProof

Bugs fixed: unification were not really explicit-named-substitutions aware.
It just compiled.

Variables can also be instantiated.

- cicParser interface changed
- get_obj now has a better behaviour when an unchecked object is retrieved

- metasenv is now checked
- the last commit introduced a bug: the debrujin function was called on
  the type of a constructor _before_ removing the left parameters. Fixed.

- parser improved: constant uris and variable uris are now handled differently
- the callback function must now return a URI and no more a term
- explicit named substitutions (with syntax { V1 := t1 ; ... ; V2 := t2})
  implemented

- cicParser interface simplified

- for/of attribute no more checked ;-(
- parsing does not require any more the current uri (that was unclear
  for CurrentProof)
- as a consequence of the previous change the parser should now be reentrant

New attribute @params for variables.

The fact that an object is trusted is now logged.

Cooking is no more required. Now we have explicit named substitutions!

cicCooking.ml* forgot in the previous commit

- Porting of all the code to the new DTD format (with, among others, explicit
  named substitutions)
- Porting to the new version of Pxp
- Porting of the cicReductionMachine code (that was abandoned for a while)
- Removal of all the cooking machinery
- Removal of the optimization (memoization) of the computation of recursive
  arguments of constructors. Required to implement the next point. The actual
  performance loss is minimal.
- First prototype of an environment with trusting abilities.

Notes: unification is still untested and probably wrong w.r.t. explicit
 name substitutions.

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

Modified some wrong paths

Written function that produce the variable "ConstantTypeUrl" used by objcontent.xsl

When printing the body of a constant, the type is also printed.
Requires the $ConstantTypeUrl variable set in rootcontent.xsl

- removed checkings for objects Definition and Axiom.
- inserted checkings for objects CostantType and ConstantBody.
- modified mode of view params (not "path/varname.var" but "varname").
- modified checkings for term LAMBDA, LETIN, PROD (with insertion of checkings for decl and def when used by these terms)

New DTD for the new exportation procedure.

Synchronization with the main branch: proofcheckerURL param added

New DTD for the new exportation module.

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

tactic update

Modified Files:
1) grammar.txt: added parentesis to string-set