changed reduction tactics ast

snapshot

Fixed an hidden occur check problem: when a Meta is being delifted,
apply substitution on the fly and delift the result. Previously we did
not recursively check the instantiation of the Meta.

added dummy entry in CicAst: UserInput

snapshot:
- changed interaction model

bumped changelog line to match upload date

disabled debugging info

parse Baseuri command

added Baseuri command

commented out some timing messages

snapshot, notably:
- fixed "noshow" bugs in sequents notebook and proof window
- implemented interpretation choice

* compressed statistics committed

- split compound fields
- rounded to integer floating point values

* snapshot

Aggiunta l'introduzione alla prima sezione:.

* output of XML file size

* fix bug detect blank nodes
* output of file size

* added stylesheet to render the results

added filling of no_concl_hyp

added query to fill no_concl_hyp table

formatted

* depths now in hash table

* snapshot

* added a few calculations

* added .cc program (and equivalent .xsl stylesheet) for collecting
  statistics about XML files

First draft (introduction).

...

filled toolbar and implemented buttons behaviours

ported to new cut and letin "API"

- added Tactics module as a common point where tactics could be accessed

Auto moved to a new file autoTactic.ml
Added a hastbl of duplicates in the library (currently filtered by
hint).

New version(s) of hint. One more stable (hint) and one more experimental
experimental_hint. The latter uses apply_verbose, since it needs to
get back the subproof of the goal, usually not returned by tactics.

Added a new boolean parameter "facts" (default=false) to most of the
methods. The idea is that when facts=true search should be restricted
to facts (theorems without hypothesis). To be used at the maximum
depth of automatic tactcis.

Porting to the new version of auto.

snapshot (notably: ported to mysql instead of dbi)

no longer use Dbi module but directly use Mysql module since it's 13
times faster

added Auto parsing

added Auto and Hint tactic

* substitution are not rendered by default, an action is generated

renamed Http_client to Http_user_agent to avoid clashes with Gerd's
netclient since both Netclient and ocaml-http are used, believe it or
not, by xmlrpc

ignore typecheck_uri{,.opt}

added test script for typechecking URIs given on STDIN

- equality test on terms before trying convertibility now first tries
  phyisical equality between terms and then fallback to structural
  equality (same behaviour of ocaml < 3.08)
- changed behaviour of are_convertible. Before this change: equality was
  first tried on terms (as above) then, in case of failure, equality
  between weak head reduced terms was tried. Now weak head reduction is
  always performed. This change is motivated by the convertibility
  between "sin x" and "cos x" (no one was able to see the end of this
  test case). Now this test case completes almost immediately and
  regression test type checking the whole standard library does not
  shown any sensible slow down

snapshot, notably:
- ported to Dbi disambiguation
- started implementation of coqide-like script window

Bug fixing.

bugfix: implemented interactive_user_uri_choice (trivial non-"advanced"
implementation: filter out variables)

ported to latest ocaml-http

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