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

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

bug fix: handled LetIn case in simpl

mathQL modified, stderr corrected to stdout im mathql_interpreter,
new lavel assignment procedure in mQueryGenerator (uses degrees),
textual interface for mQueryGenerator added

Invariant description added.

Bug fixed: there is an invariant that every attributed uri list must be
ordered on the uri that was not enforced for the new Reference.

Wrong xpointers generated. Fixed.

Locate query changed again. There is a mismatch between Domenico's
implementation and Ferruccio's semantics. The code now conforms to
Domenico's implementation and seems to work.

class parameter added to the getallrdfuris method.
Values may be forward or backward.

Bug fixed: empty elements did not ask for the size of their first following siblings in the
charcount mode.

added comment about 0 and 1 based indexes