- handle Box.Space in textual pretty printing

- removed mandatory parens for application
- "in" and "and" are now keywords
- changed binder syntax, now more coqish
- alone symbols no longer permitted (e.g. "+" alone is no longer a term)

"in" and "and" are now keywords

splitted History module out of StatefulProofEngine

- splitted out History module
- exported all_events
- status is now a pair proof * goal _option_ so that completed proofs
  have their entry in the history and could be passed to observers
- added set_metasenv method to change imperatively metasenv
- added explicit notification method notify

xmldiff's META

moved xmldiff module away from gTopLevel

snapshot

snapshot

snapshot

bumped deps to 0.6.4

bumped version to 0.6.4

* minor correction to make the new mathml widget work better

* the transformations have been ported so to generate BoxML + MathML
  instead of MathML alone. All the affected files have been heavily
  changed both in the interface and in the implementation, many
  solutions are certainly temporary and the code would benefit from
  extensive cleanup

* removed PREDICATES
* added REQUIRES to init gtk2 properly

added initial_status

fixed parse error for ocaml 3.08

meta_closed added

fixed cictheory:/ bug (thanks Lionel for the patch)

The jsmenu is now under CVS.

* the click signal now acts on both maction (MathML) and action (BoxML)

now should run also when the db is down (untested)
(the -nodb option is still unimplemented)

bumped deps on ocamlnet to 0.98

ported to ocamlnet 0.98

ported to latest lablgtkmathview

ported to pxp 1.1.95's event parser

added hyperlinks for getalluris/ in help message

fixed some illegal backslash escapes

bug in constraint generation for variables fixed

Corrected bug about the generation of constraitns: variables
must not be indexed.

Bug fixing: the call to MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
must be done after filter_new_constants (that compares uris).

ported to ocaml 3.08

debian version 0.0.6-6

debian version 0.6.3-2

ported location handling to camlp4 3.08

fixed some invalid backslash escapes

fixed some illegal backslash escapes

fixed .mli syntax for polymorphic methods (apparently changed between
ocaml 3.07 and ocaml 3.08)

fixed some invalid backslash escapes

* porting to gtkmathview 0.6.3

* fixed bug of multiple selections
* minor code cleanup

(pre-)porting to gtkmathview 0.6.3 && ocaml 3.08

* update to version 0.6.4 of the widget
* not tested

ported to ocaml 3.08

ported debian stuff to ocaml 3.08

The type substitution has been moved into Cic.

Subst has been added to the kernel.

* split evil let definition (ic, oc) = ... into two subsequent
  definitions
* using Gzip.open_in_chan to avoid file descriptor leak

Modified filtering function

cleanURI now removes also the part that follows the '#' symbol.

The URI passed to the control frame must be clean (i.e. no #xxx part).

The part after # must be removed for the control frame.

Bug fixed: beta_expand did not perform any recursion over the local context
of a metavariable ==> the local context was not lifted.

commeted out some debugging instructions

commented out some debugging instructions

Bug fixed: eta_expand did not perform any recursion over the local context
of a metavariable ==> the local context was not lifted.

Bug fixed: the beta_expansion function did not lift the argument before
attempting to match it ==> no matching was done correctly under an
abstraction.

...

New handling of substitution:
- splitted metasenv from substitution
- substitution enriched with canonical context information for
  checking_metasenv_consistency

added (commented) benchmarking code for the disambiguation paper

removed a useless test on explicit substitutions on variables with body

use get_obj to retrieve cic objects instead of typecheck

fixed typo

- new implementation of the apply case in fo_unif using beta expansion
- infinite loop fix while unifying terms in an invalid metasenv

ugliness changes:
- more google like look and feel for query results
- exceptions are no longer rendered in <h1> elements but pretty printed
  inside the standard moogle HTML template
- advanced search status is now rememberd between searches
- added results count
- added result type feedback in results page

Corrections to "auto" tactic

elim_tac rewritten almost entirely. It is now based on refinement +
one invocation of the (now more powerful than before) apply_tac.

Added new function compare_metasenvs.

Comments changed.

- In the case (?i args) vs term the term is now eta-expanded w.r.t. args.
  This allows to easily implement elim using apply and it makes the auto
  tactic much more powerful.
- CicMetaSubst.apply_subst semantics changed: it now always performs
  beta-reduction when a meta in head-position in an application is istantiated
  with a lambda-abstraction.
- CicMetaSubst.apply_subst_reducing no longer in use: removed.

New syntax.

Fourier URIs changed in V8.

- moogle replaces the old search engine

bugfix: ignore proof checker output

atmost/atleast/exactly constraints are now used only for the "hint" method.
They are no longer used for "match" and "elim".

in the particular case of simple searches, Andrea atmost/atleast/exactly
technique is used

first moogle commit

search.xsl added.

Added search.xsl (S).

Stylesheet whose input is an empty document. It calls the
new search engine (moowgle) passing the needed parameters.

New profile param: searchengineURL

Uncommited changes committed.

Interface URL can now be setted using the control panel.

Interface URL can now be setted.

The normalization of URIs when the DB is empty (or it is being filled) is
not reliable. As a consequence the semantics of the Http_getter_map has been
changed again: the only method that normalized the URIs before using them
is the resolve method. The methods replace, add, remove, etc. no longer
normalize their argument.

- new stylesheets in the predefined set
- some fields are now password fields

New attributes for ht:* elements proposed by Nijmegen.
All the attributes are IMPLIED and the default value for all of them
is backward compatible.

Objects ordering is now case-insensite.

fix for proofEngineTypes.mli

new universes implementation

Ordering is now done in no-case style.

theory:path/index.theory are not rewritten to theory:/path.theory
if theory:path/index.theory exists in the database.

New filtering function for "Auto" tactic using "just costraints"

Back compatibility code introduced:
 1. the ls method maps a theory theory:/path/filename.theory
    to theory:/path/filename/index.theory iff there exists at least
    one object of the form cic:/path/filename/*
 2. the getter handles every URI theory:/path/filename/index.theory as
    the normalized URI theory:/path/filename.theory

The theory index.theory, if present, is shown at the beginning of the
listing.

* makeProofTreeURL ported to the new interface

.body removed from bread crumb trail

Links in the control frame when the URI ends with .body are now handled
correctly (i.e. the .body is removed if meaningless, as for the proof-checker
or the metadata).

<xsl:import href="toplevel_header.xsl"/>
moved here from show_dc.xsl

<h1> ==> <h3>