Now esempi/fourier.cic end with a proof!

- used change_tac to change from a->False to ~a just before tac2.

Fix: Ad hoc change_tac may not work sometimes. check what Cic.Anonimous means.

Bug fixed: I don't know what the bug was exactly, but it happened that
the connection was not closed when using some HTTP 1.1 clients (e.g. wget)

mqint.ml patched

topLevel updated to use mqint set_database and get_database

Bug ``fixed'': we do not need to apply sym_eqT since the goal we produce
is already 1^-1 = 1 (while Coq produces 1 = 1^-1).

- matql_interpreter_galax branch removed once and for ever
- added the dependency to natile-galax. You need to add
  /projects/helm/galax/sources/natile-galax-0.1-alpha-installed/lib
  to your OCAMLPATH to make it compile again.

Switching interpreter patched, addedd:
 postgres_db
 galax_db
 get_database

The two interpreters are now both in mathql_interpreter. The one actually
used can be choosed setting a global reference.

No more useful

Old modules (use.ml/mli, eval.ml/mli,...) eliminated.

Switching interpreter.

Comments reindented.

Merge of the new_mathql branch with the main branch:
 - new query language
 - new interpreter for the new query language

NOTE: the galax version of the interpreted is not ported yet (and does not compile)

Merge of the new_mathql branch with the main branch:
 - new query language implemented
 - the locate query is now bug-free (and a _LOT_ faster)

- indentation is now in pseudo-functional style!

- rewritesimpl_tac added in fourierR.ml (wrong location)
- simpl_tac added in fourierR.ml (wrong location)
- "RewriteSimpl ->" button added
- "Rewrite ->" button removed

- write_tac fixed (the list of new goals was empty)
- some new bugs introduced here and there ;-)

A tough test for rewrite.

- bug fixed: some liftings were missing in the implementation of rewrite
- new feature: rewrite now works up to alpha-equivalence

- rewrite extended to handle rewritings with eqT
- equality_replace implemented (based on the new rewriting tactic)

Trivial bug in equality_replace fixed: an exception was raised in spite of
returning false.

New tactic rewrite implemented.
Not tested yet.

- idtac used for debugging removed
- bug fixed: the natural number 1 was mapped to (Rplus R1 R0).
  It is now mapped to R1 (as it should be). This close all the
  residual bugs.

Still to do: we need to close the last open branch using equality_replace,
as soon as it is implemented.

More debug printings.
Replacing the wrong tac with id_tac it goes straight to the end,
lefting 1 more goals open:
0 < (1+0)/(1+0)

Remember that the tactic fails applying
0<1 to 0<1+0

Use patched.

Added an example to test fourier_tac.

Debug printing update, now the unification bug
seems to be in tac_zero_inf_pos.

We get '0 < 1 + 0' instead of '0 < 1'.

Handling of the splitting of constants into body + type.

Handling of the splitting of constants in body + type.

HTTP_GETTER_PORT environment variable added

Several bug-fixes:
 - apply_tac and my_cut used to generate a new metavariable without
   updating the metasenv
 - a boolean "false" was used in place of the propositional "False"
 - minor fixes

The equality_replace tactic is completely wrong. For now the whole
proof branch that needs it is commented out.

Open bugs:
 Some unification problem in the proof that the linear combination can
 be derived from the initial disequations.

Pretty-printing of MUTIND and MUTCONSTRUCT with crazy indexes fixed.

added bootmisc and tomcat scripts

added support for unload and reload of predefined stylesheets

script that loads predefined uwobo stylesheets

added /etc/init.d/ stuff

Web-services ordered by port number.

DRAW_GRAPH_PORT environment variable added

URI_SET_QUEUE_PORT and DRAW_GRAPH_PORT added

Default ports changed.

URI_SET_QUEUE_PORT environment variable added

proofcheckerURL configuration parameter added

proofcheckerURL param added

fourier_tac without useless recursion

- The Getter and UWOBO moved to mowgli.
- The UWOBO default port changed to 8081.
- The Getter default port changed to 48081.

- New environment variables set.
- Configuration files for V7_mowgli now also generated.

hopefully last tactic update cvs log

Initial revision

HTTP_GETTER_DTD_BASE_DIR configuration parameter added

tactic update

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

Better handling of queries. Now both the locate and backward queries give
the user the possibility to disambiguate the answer, and write it in the
input window. Some bugs in the disambiguation process have been fixed.
Finally the output of the query process in the outputhtml window is now
much more verbose.

Modified Files:
1) grammar.txt xmathql.dtd: relation modified

change code moved to change_tac (functional version defined in primitiveTactics)

Modified Files:
1)grammar.txt xmathql.dtd: updated versions
Removed Files:
1)core_grammar.txt: now all the grammar is implemented

commit of galax mathql interpreter

Tactic update

Small code improvement.

Tactic update

new query generator

List of tactics implemented and to implement (italian only).

restricted mode to use when the database is down :)

query generator timing feature improved

Modified Files:
1) schema-h: Prop. occurrence removed

ring.ml* splitted into ring.ml* and tacticals.ml*

then_ tactical implemented (equivalent to the tclTHEN of Coq)

Modified Files:
1)schema-h: added prop. coercion

Fourier tactic update

When locate is used during the lexing phase, it may happen that no URI is
found or more than an URI is found. In those cases a window is now opened
and the user is asked to either enter the URI (if none was found) or
choose from the list of found URIs.

Patch applied to the locate query: when used to retrieve the first inductive
type of a mutual inductive types block, the returned URI is now the URI of
the type (with the fragment identifier!) and not the one of the block (without).

Fourier tactic update

First works

Added Files:
1)schema-h schema-hth: new versions
Removed Files:
1)schema-h.rdf schema-hth.rdf: old versions

mQueryGenerator and topLevel patched

Modified Files:
1)dces dcq dctype: new versions
Removed Files:
1)eor

some small improvements: command line sintax changed, -MB added

Modified Files:
xmathql.dtd: syntax error

The parser (the lexer indeed) now use the locate query to locate an object
whose identifier is unknown. In ambigous cases, no choice is given to the
user and the usual exception (identifier not found) is raised. It works
only for constants and for the first inductive type of a mutual inductive
type block.

raw HTML markap generator

textual parser fixed

Fourier tactic

Added Files:
1)result.xml xmqlresult.dtd: example and dtd for MathQL query results

user name added to tmp file name

Modified Files:
1)core_grammar.txt grammar.txt query.xml xmathql.dtd: new grammar

Type expression simplified.

Comment typo fixed.

Modified Files:
1)core_grammar.txt grammar.txt query.xml xmathql.dtd: new version
----------------------------------------------------------------------

debian release -3

debian version "-8"

forward compatibility changes for ocaml 3.06

Interface file created. Missing from previous commit.

Updated to use the new parser that creates (stacks of) existential variables
when an implicit arguments is found.

Updated to use the new parser that creates (stacks of) existential variables
when an implicit arguments is found.

Many improvements in tactics (and tactical) representation:
1) tactics are no more functions from state to state, but functions from
   proof * goal to proof * goal list where the goal list is the list of
   new goals generated
2) proof and goal are no more optional
3) all the tactics have been slightly changed so that their type is now
   param1 -> ... -> paramn -> ProofEngineTypes.tactic
4) the tactical thens has been implemented

Other changes:
1) more .mli committed
2) comments and copyright notices added where missing

First version of hxsp (new version of UWOBO implemented in Perl by
Alessandro Barzanti using the bindings to libxml and libxslt).

Added examples.

converted to unix textfile (fromdos)

bugfix: Ring will work again with varmaps :-)

- added Ring tactic on reals
- module splitting
- proofEngine is now almost functional

bugfix that inhibit the removal of certain hypotheses