implemented pagination

rebuilt

- bugfix use disambiguator metasenv for initial proof status in hint
- use configuration file from /etc
- catch Chat_unfinished
- removed ancient debugging messages

added CSS information for (forthcoming) bottom bar

sort hint's result accordingly to the "least goal left first" principle

bugfix in cmatch constants_no now consider also the number of types of
main

- added var selection boolean to locate
- added cardinality constraints checking to match_term

added vars selection boolean on locate

- reimplemented basic features using the helm-metadata library instead
  of MathQL. Previous version has been tagged "moogle_mathql"

implemented elim query

added Hint "tactic"

bugfix: handle overflow in powerset cardinality

no longer builds by default tex_ and cic_textual_parser

- reimplemented tacticChaser and friends in term of Metadata module and friends

- support also DBI handle
- no longer use MQueryMisc

no longer build oldDisambiguate

uses DBI handle

- disambiguation now needs DBI handle
- no longer build by default old cic_textual_parser

auto needs DBI handle

temporary: for the moment we need both MQI handle and DBI handle

ported to Dbi-disambiguation

ignore boolean returned by saveDocument

- added (hack) apply_tac_verbose (for auto)
- ported to typed explicit subst

- changed metadata type so that positions contains depth
- introduced constraints (vs metadata)
- positions no longer hard coded (so that both short and long names are
  supported)
- added "where" parameter so that matching could be perfomed either on
  conclusion only or on the whole statement

removed reference to MQueryMisc

- removed MQueryMisc. Ratio: it was used only for transformation uri -> term.
  The same feature is now available directly in CicUtil without the need
  of cic_textual_parser URIs

- no longer depends on MQueryMisc for term_of_uri
- disambiguation now uses MetadataQuery instead of MathQL

no longer depends on MQueryMisc

- ported to new getter API
- implemented remove_term

ported to typed explicit subst

removed dependency on cic_textual_parser where this dep was used only
for term_of_uri, now in CicUtil

describe exception raised by term_of_uri

removed old function term_of_uri (now in CicUtil)

be more quiet (removed debugging prints)

ported to typed explicit subst

rebuilt

- 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