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.

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