- ported to typed explicit subst
- beta expansion in the case of Appl commented, waiting for a better
  solution

- ported to typed explicit subst

- ported to typed explicit substitutions
  (this implies that kernel wrappers which used to handle substitutions
  are vanished)

- ported to typed explicit substitutions

cleanup temp files on parser failure

- reimplemented meta_closed in non CPS way (faster!)
- ported to typed explicit substitutions

added type to explicit substitutions

- use CicUtil.term_of_uri instead of deprecated HelmLibrayObjects
  similar function
- reverted to old syntax for binders (e.g. \forall x,y:nat.x=y)
- use ";;" as phrases terminator

- bugfix: sequences like ".(" are now lexed, correctly, as
  [ SYMBOL "."; PAREN "("] instead of [ SYMBOL ".(" ]

use helm-cic_textual_parser2 findlib package when building tests

added dep on helm-metadata

bugfix: use only baseuri in uri part of MutInd and MutConstruct

use latest Http_getter module API

- API change (renamed some exceptions)
- ported to the latest PXP version

added reference to MetadataQuery (now it builds properly)

implemented in place old Filter_auto filtering

fixed a buggy pattern matching

- split metadata type in metadata and constraints. Metadata are computed
  from cic objects while constraints are used to query the database

- removed cic_cache and cic_annotations_cache
- moved metadata before tactics

added term_of_uri

snapshot, still work in progress

top level query module

broken

removed cicCache (cicEnvironment should be used instead)

implemented here at_least constraints matching engine

added helm-metadata module

removed some old debugging messages

moved string_of_uriref to UriManager

moved string_of_uriref from MQueryMisc to UriManager

Luca (bugged) debugging stuff removed.

fixed make dep command

no_inconcl_aux managed

* create_mowgli_tables.mysql.sql added
* fill_inconcl_aux.sql added (what does it do? Ask Andrea or Selmi)

snapshot

added alias for cic_textual_parser2

snapshot, notably history no longer remember annotations: they are
computed on the fly

transformations no longer use Content_expression, but rather CicAst

pretty printed Absurd's term

added term argument to absurd

get_and_save now handles big files properly (i.e. doesn't hold them
entirely in memory)

ported to ocaml-http 0.0.10 (renamed Http_client -> Http_user_agent)

setting goal doesn't change history status

added new Utf8Macro module

Added -syntax support (if needed, use OCAMLC_P4 instead of OCAMLC in
Makefile); ocamldep uses it by default.

added utf8_macros

moved utf8 macro handling to the new module Utf8Macros

fixed typo

new module: expansion from tex like macros to utf8 strings

snapshot (notably: implemented "check")

added dependency on helm-xmldiff

moved xmldiff in ocaml/

- added xmldiff module

added Undo/Redo commands

- fixed "Blue" vs "blue" typo

- 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.