added clean_and_fill, to be invoked on qed

snapshot, not yet completed, but ...

- added support for contexts (terms with holes)
- added CicUtil.pack/unpack to pack/unpack several terms in a single term
- added CicUtil.strip_prods to removed a given number of head prods from a term
- added CicUtil.context_of/select to create contexts/select a subterm
  matching a context

cosmetic changes

added begin list and end list comments to help moogle search engine plugin

exported lift_from

snapshot

added an hyperlink to the input syntax page

improved input syntax page with example queries of elim, match and hint

added URI printing in the result page (so that mouse-over is not the
only way to know the URI of results!)

first commit (in the wrong place --by CSC) of induction principles generation

ignores example binaries

ported to new format of Parse_error exception (which includes error position)

(dummy) porting to universes

implemented pretty printer for (mutual) (co)inductive types

(first) complete implementation of (mutual) (co)inductive types syntax

addded inductive definition to AST

- enriched Parse_error exception with error location
- first implementation of inductive type definitions (not yet completed:
  mutual inductive definition are still missing)
- test parser now displays error location using ASCII escape coloring

symmetry of equality NOT used in auto

New version of auto with "width".

snapshot

moogle syntax help page, actually contains only syntax and examples for
the "locate" query. "hint", "match" and "elim" syntaxes are currently
undocumented

changed "locate" so that it supports shell-like pattern matching with
'*' and '?' wildcards

ported to universes

*** empty log message ***

sync with universes and ~subst (and not ?(subst=[]))

Added universes handling. Tag PRE_UNIVERSES may help ;)

Added universes handling. The PRE_UNIVERSES tag may help ;)

Bug in the management of substitutions into auto corrected.
No significative loss in performance.
Comments commented.

- ported tests to newer PP / substitutions

- passes subst to FreshNameGenerator
- removed some old debugging prints

removed old debugging prints

passes ~subst to FreshNameGenerator

passes subst to FreshNameGenerator

- pass subst to FreshNameGenerator on mk_fresh_name invocations
- removed assert failures on get_cooked_obj (rolled back last commit)
- reindented (the huuuuuuuge) eat_prods function

bugfix: FreshNameGenerator uses the type checker on mk_fresh_name
invocation, thus it should receive in input a subst to be passed to the
type checker in order to avoid "unknown" Metas in the term to be type
checked

bugfix in type_of_aux' which erroneously discard given substitution
(fixes a lot of CicUtil.Meta_not_found spurious exceptions)

ported to Mysql

ported to new xpointer syntax

protected invocations to get_cooked_obj with assertion failures

protected invocations of get_cooked_obj with assertion failures

guard get_cooked_obj calls with assert false in case of Not_found

use get_obj instead of get_cooked_obj in order to retrieve params for
unchecked objects (fixes "not found" bug when trust in the environment
is false)

* several adjustments after introduction of the depth column

* validation scripts

* basic infrastructure for collecting statistics

added parse test for
- expat
- libxml2 (xmlreader API)
- libxml2 (SAX2 API)

set environment trust to false to avoid dummy proof checking

use stateful logger so that the ProofChecker daemon is able to properly
indent proof checking messages

added a stateful logger which remember indentation level of recursive
type checking

added set_trust to externally set the trust function (used by the proof
checking daemon)

ported to Mysql native connection

Resolved problem occured when "=" in MainConclusion

Removed duplicated uri in sigmatch

Bug fix

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.