added HBugs interface module for gTopLevel

rebuilt

removed tmp_dir no longer needed (it was used only by ClientHTTP module)

bugfix: use temporary file name to avoid file access clashes when the
same teporary dir is used by many processes

- added pp_to_outchan and pp_to_string for other medium pretty printing
- factorized implementation of pretty printers so that it's used by all
  pretty printing functions

Makefile patched

Makefile.common.in and .depend backtracked to my last commit (before the
ones of Ferruccio) and then modified. Dependencies between a file and a
library are now handled correctly.

packege dependences calculation patched

package dependences calulation fixed

SQL quoting fixed in relation.ml

Added new module DiscriminationTactics

Added buttons for new tactics Injection and Discriminate

Added module DiscriminationTactics with brand new tactics Injection and
Discriminate, both working only in simple situation

patches for the new interface of text_of_query/text_of result

new interface for text_of_query/text_of_result + bug fixes

Dependency simplification.

Minor module re-organization:
1. SequentPp is now no more dependent from proofEngine
2. the functions to apply stylesheets from DOM documents to DOM documents
   are not any longer exported by ApplyStylesheets

...

The scratch window is now based on the sequent_viewer widget.

Major module reorganization:
- new module TermViewer: holds widgets to render and interact with sequents
  and proofs at the CIC level
- new module ApplyStylesheets: functions to apply stylesheets and map
  terms and sequents to MathML Presentation
- new module InvokeTactics: it is a functor that gives back a module that
  defines one callback function for every tactic

1. helmns and domImpl moved to the misc module ;-(
2. all the constants and functions relative to stylesheet applications have
   been moved to the new module ApplyStylesheets, whose interface is really
   minimal.

Minor code reorganization:
 1. several functions unrelated do disambiguation moved from Disambiguate
    do Misc.
 2. TermEditor module added. It implements a widget for entering terms.
    The widget is also responsible for the disambiguation.
 3. TermEditor is now the only widget that uses the Disambiguate module.

Tactics button rearranged.

Clear and ClearBody moved to the pop-up menu.
No check is done so far to avoid activating them when the selected "term"
is not an hypothesis.

replace_lifting generalized to the simultaneous replacement of n terms.

ProofEngineHelpers.mk_fresh_name now used in place of "dummy_for_rewrite".

1. Added a callback to the generalize tactic to generate a fresh name.
2. Dead code removal in various files.

Added a callback to the generalize tactic to generate a fresh name.

Generalize now works on a list of convertible terms, generalizing all of
them at once.

Generalize tactic moved to the contextual menu.

New: we now have a new pop-up menu for the reduction tactics.

1.  All the reduction tactics have been modified to reduce several (sub)terms
    at once.
2.  To reduce several (sub)terms at once you can use the new multiple
    selection feature.

All the reduction tactics have been modified to reduce several (sub)terms
at once.

Multiple selection is now enabled in the goal and check windows.
All the tactics still behave as before.

maction toggle restored

Optional callbacks have been added to tactics that need to introduce
new fresh names directly (i.e. without calling other tactics that need
fresh names). The default behaviour is _MUCH_ nicer than the previous
dummy one and is fully functional.

Corollary 1: all the code of tactics.cma is now reentrant.
Corollary 2: the user can be asked the fresh name if it is requested
             by a top-level tactic.

Dead code removed.

Decompose now has a new parameter which is the callback to call to select the
uris that must be used for the decomposition.

Decompose now has a new parameter that is the callback function to call
to select the uris that must be decomposed.

Fixed. It was no more working since the move of the tactics under the ocaml
repository.

added META for module helm-tactics

moved tactics from gTopLevel to the new module ocaml/tactics

moved tactics in ocaml/tactics

* very small fixes here and there

Added Decompose tactic

bugfix while printing MutInd and MutConstruct unresolved uris

added html templates and pages

- disambiguation implemented!

- added references to gTopLevel needed modules

New module Disambiguate to hold:
 - a functor to disambiguate terms. The input module holds all the
   callbacks to the user (that will be implemented differently in Gtk
   and as Web forms).
 - some utility functions working on CicTextualParser0.uri which should
   be moved somewhere else.

typo: ')' mismatch

Ambiguous parsing improved: refining is now used to prune-out not-well-typed
choices as soon as the term can not be refined. Unfortunately the whole
disambiguation is parsing-bound and not type-checking/refining bound.

Refine can now also raise Uncertain. The exception is raised every
time a metavariab le could be instantiated in such a way that the
term could become well-typed. Useful for ambiguous parsing.

The interpretation function can now return also "Implicit".
Useful for incremental ambiguous parsing.

New: refinement is now used to disambiguate parsing.

New constructs \x.T and !x.T introduced. They require refinement.

* First implementation of CicRefine
* unwind_subst is now exported in the interface

* if no configuration file is found, issue a warning but doesn't crash

"Insert Query (Experts only)" menu item added.

Added a special charcount threatment to the 'append' csymbol (whose length
was estimated being 6 instead of 3). We should do the same for every csymbol
we provide special notation to.

MathQL textual lexer patched
topLevel patched for compilation: -B and -MB don't work

Wrong commit undone.

Last commit before major modifications to do.

Rearranged tactics in VariousTactics into new modules EliminationTactics,
EqualityTactics, IntroductionTactics and NegationTactics.

Minor widget rearrangement.

notation "@" for append added

Added an almost working version of Generalize tactic.

Added an almost working version of Generalize tactic.
Added yet another version of replace, useful in Generalize.

Rearranged tactics in VariousTactics into new modules EqualityTactics, EliminationTactics,
IntroductionTactics and NegationTactics.
Added new tactics: Rewrite <-, Replace.

Severe bug fixed: the test failed in the case of (Rplus (...) R1).
As a consequence (Rplus (Rplus R1 R1) R1) was rendered as 2.

* Partial checking of mutual inductive definitions allowed.
* New environment variables requested:
   GTOPLEVEL_PROOFFILE
   GTOPLEVEL_PROOFFILETYPE
   GTOPLEVEL_PROOFFILE
   GTOPLEVEL_PROOFFILETYPE
   POSTGRESQL_CONNECTION_STRING

Unary minus now rendered without parentheses.

"Rewrite ... with ... by ..." line-breaking handled.

First experimental commit of the notation (partial!) for real numbers.

Ring partially ported to the new library. But I am completely sure that
this is not the notation we need for ring. To be changed...

Bug fixed: beta-redex transformations to LetIn were bugged when the lambda
had two or more decls.

cut & paste typo fixed

positive.xsl is now included in headercontent.xsl and no more required in
arith.xml and list.xml. This is necessary to overload the standard rendering
of some operators (e.g. notation for real numbers).

Now "only" constraint are more restrictive.

* ElimSimplIntros replace by ElimIntrosSimpl. Simplification is performed
  only in the conclusion and not (yet) on the hypothesis.

* New button "Select only constants" to choose the URIs to try during the
  disambiguation phase. Usually the number of constants is small and among
  them there is the right URI.
* New ElimIntrosSimpl replaces the old ElimSimplIntros.

Simpl now handles let-in reductions as delta-reductions. Cool.

* mQueryLevel2.get_constraints now gives back only the "must" constraints.
* the "refine constraints" interface has been improved. It can now handle
  also constraints on Sorts and constants.

New notation for ListSet. It often raises ambiguity problems in theorems
that also use the same notation for PolyLists.

instantiate for inductive principles covered

instantiate for induction principles covered.

Bug fixed in binary standard MathML Content operators: the href/xref
attributes were not generated.

...

The fresh_name generator has been moved to ProofEngineHelpers.
intros_tac now directly uses it ==> no more ~mkname arguments.
The generator has been "improved" so that it does not generate any
more two equal names. The drawback is that every identifier is
augmented with a nonce.

Comments removed.

Bug fixed: when iota-expanding fixpoints the context was sometimes augmented
with the new types, even if the expansion already de-lifted the function body.

mQueryLevels2.mli added in Makefile.

The user interface for the completeSearchPattern query has been improved.
It is now "easy" to query for induction principles, for example.
Much work still to do.

1. depth constraints for Rels and Sorts are now optional
2. "can" constraints renamed to "only" constraints
3. several bug fixes:
    * the order of arguments for Sub in the second phase of the query was wrong
    * some identifiers in the generated query were unbound

1. The depth constraint on Rels and Sorts is now optional.
2. "only" (ex "can") constraints are copies of the "must" constraints

A simplification bug was introduced during the clean-up before the last
commit. Fixed.

Notation for if then else.
Other bug fixes.

Bug fixed: the lhs part of an explicit name substitution was not generated
as an m:ci, but as simple text ===> no m:mi and no hyperlink were generated.

Minor bug fixes in the 'instantiate' element handling.

Showing a query result which was an inductive type or constructor was bugged.