proof of concept implementation of scripts highlighting, grafite.hrc is still bugged

snapshot

added $Id$

use the graphviz pretty printer to generate graphviz markup for the coercions graph

moved graphviz pretty printer outside matita, so that it can be used by other components (e.g. from CoercDb to generated coercions graph)

use lablGraphviz to render the coercion graph and added a callback to follow hyperlinks there

generate dot files with attributes on nodes (instead of only edges), and added generation of the href attribute

added uri_of_carr

added pretty printer for dot files (it may need to be moved elsewhere in the future)

fixed the number of columns in the clusters table

Documentation date changed.

More commands documented.

bugfix: remove all generated temp files

added widget for rendering and interacting with graphs generated via graphviz

More commands documented.

More commands documented.

First skeleton of documentation for "other commands".

Missing copyright added to tactics/declarative.ml*

GrafiteAst.Quit (unused) removed.

GrafiteAst.Print (unused) removed.

GrafiteAst.Search_pat and GrafiteAst.Search_term (both unused) removed.

restored the 2 ways of pasting: both "as term" and "as pattern" are available again

paramodulation is not a stand alone tactic: doc fixed.

More documentation.

dependences updated again :)

updated dependences

First experimental version of the declarative proof language for Matita.
Supported commands so far:
  assume id: term
  suppose term (id)
  by term done
  by term we proved term (id)
  we need to prove term (id)

More TODO items in the documentation.

- removed Positive and Negative (all is positive)
- eq_f and eq_f1 used in proofs

fixed

...

- cheanges for the new coercion stuff (including the generated graph)
- new test for coercions
- new test for tinycals

renamed the coercion

improved coercions support:
- multiple coercions from the same carrier are allowed
- coercions are hidden from the proof too
- a new function to print proof in text mode added

fixed 1,2: and *: according to the camera ready semantics

added flatten_map

eq_f1

megatheorem (even if unused)

fixed *: and n,m:

...

bugfix to developments:
- if an included .ma file is not found (not in CWD, not in include_paths)
  an error is issued
- if an included .ma file is found but the corrsponding .lexicon is not found
  a development for the .ma is searched:
  - if found it is used to compile the .ma file
  - if not found the user is aked to create a devel for the file included
    (and not the file that he is editing, that may not be in the same devel).

Instead of closing the socket to avoid persistent connections (a bugged
solution in Ocaml 3.09.2), we use the new ~auto_close feature of libhttp-ocaml.

when auto_close is set, use flush + shutdown instead of close_out, work around an ocaml 3.09.2 bug

/....

...

- patch to consider the symbols of the goal when computing the weight of an
  equality.
- actives simplified during fwd/back are not appended (but put in front) of the
  passive list

Documentation of tinycals started.

pretty proofs are back

fix

"linear" keyword inserted (used by lapply)

Cleaning up; removed a couple of "open".

...

Demodulate used to be a reduction_kind and it used to take a ~pattern.
Since demodulation is not a reduction kind, I changed it to a normal tactic.
Moreover, since the ~pattern was unused, I have temporarily removed it.
Doc changed accordingly.

WORK IN PROGRESS:
First commit of setoids.ml* (a porting from the Coq code by Claudio Sacerdoti
Coen).
The file setoids.ml is now compiled (and linked), but it does not provide any
functionality yet.
"(*Coq" comments are used in several places for parts of the code not ported
to Matita yet.

before goals are inferred with current,
we demodulate them with active+current
(was: only with current)

Documentation for variant fixed (the type and body are NOT optional).

goals after a superposition step are relocated

- "linear" flag added to lapply (automatic clearing)
- RELATIONAL-ARITHMETICS updated to use this flag

karma: every term the rewrite acts on must be substututed

fix

fix

fix

fixed gzip usage

superposition_left not performed if the input goal is an identity

fix

csc trick on steroids

new mega spreadsheet available

fix

added gzip to log files

- decompose now runs with no arguments (operates on the whole context)
- clear now takes a list of hypotheses (clears each)
- RELATIONAL-ARITHMETICS updated to use the new tactics
- tactics/Makefile fixed to correctly build tactics.mli

fixed infer_goal, added simplification before inferring with current

using the new metadataConstraint function

used the new metadataConstraint function to retrieve equalities from the library

fixed equalities_for_goal

the old compute_eq_weight is back (no more max)

fixed generation of letins

added a metas_of_term implemented using sets instead of lists (avoids some stack overflows)

file names patched

patched

more work for the generic auto parameters

added the geniric
  auto params
syntax and the auto superposition tactic

forgotten commit

RELATIONAL-ARITHMETICS updated

- fwd concrete syntax fixed
- decompose, fwd, lapply documentation fixed

garbage collection of dead equalities implemented

- added some documentation on the fwd tatcic
- lapply concrete imput syntax fixed

Patterns are now documented.
But: how do we do multiple selections in matita?

axioms removed

hack to allow (**)

typo cpying the formal semantic

reorganized guiven_clause to work with the on_the_fly simplification of goals during ghr infer_goals step

demodulation of goal activated again.
to deactivate it, the check_if_goal_set_us_solved should be moved after the infeer_goal step

some experiments

added (but still unused) remove_local_context

added (but not yet used) remove_local_context
weight of non oriented equations decreased

Utils.compare_terms instead of compare_weights
fold_right -> fold_right

occur_check and unification fixed. now Meta(i,[]) and Meta(i,[...]) are
considered the same.

...

- some fixes regarding URIs of equality that now should be coherent with the
  one of the goal
- eliminated the stack overflow issue when building the proof

instead of including library_notation we include logic/equality that is smaller