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.

Interface improvement: a window is opened to show objects returned by the
completeSearchPattern query.

...

*** empty log message ***

New feature: the user can now enter the list of "must" constraints he wants.

* mQueryLevels interface clean-up
* gui improvement: the precision level of the SearchPattern query is now
  chosen by the user. Previously it was guessed.

Simplification euristic improved.
It is now able to simplify a Fix which expands to an expressions which
simplifiable Fixes therein.

Completely broken parsing of Fix and CoFix fixed.

Several bug-fixes to the abstparam hell.

- reverted to only one quotation level for xmluri, libxml2 is now fixed

Variable redefined twice fixed.

Variable redefined twice fixed.

New tactic fold_simpl.

* fold_tac has now a new parameter, which is the reduction to ``undo''
* The Fold button is replaced with Fold_whd and Fold_reduce
* Minor interfaces modifications

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 &#x0A; 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