snapshot

* snapshot

* exceptionset -> exception_set

* update

* code cleanup
* added partial implementation for view

* IDL file update (and renamed)

select and click signal added

added information on the "qdl" article with C.S.C.

use an integer debugging level instead of a boolean one

- use hbugs' describe_callback to render apply-hints on selection
- sync default uri proposed while loading a new proof and loading one
- resend status to hbugs on tab change

commented out gtkmathview's font_size override

added "start" and "stop" targets for hbugs

added support for external configuration of describe_hint_callback

added "describe_hint_callback" invoked when a hint is selected

- removed useless status bar
- hid menu bar
- added (Re)Register button
- added vertical pane between subscription and hints
- changed default size to a "decent"-one

send SIGKILL to stop web services

commented out thread killing (we have to wait for a decent Thread.exit
implementation)

get_childNodes no longer used ==> major performance speed-up

Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.

added \neqt macro

added notation for Ropp and Rinv

string ==> id

Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.

fixed associativity of some (all!) binary operators

Replace is now working also over Type.

Replace tactic fixed. It was not working any longer. (It produced a dummy
eta-expansion).

Notation for Rdiv and Rminus.

Debugging infos removed.

string => id

Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.

replaced with my generic latex makefile

* update with some candidate methods

* added test View interface. It is basically empty but eventually it will host
  any gtkmathview-specific method

- added a destroy callback
- ignore delete events on hbugs window
- unsubscribe only when hbugs window gets _destroyed_

start tutors with nice at the lowest priority

avoid deletion of useful .cmi with .PRECIOUS

commented out debugging tutor "wait"

- added dot notation for real numbers and basic operations on them
- added support for \eqt

- added default URI for new theorems
- added menu items to the hbugs menu for:
  * start and stop hbugs web services
  * force submission of current status

added support for X11 clipboard pasting with CTRL-V shortcut

added methods to start/stop web services

added eqT's macro

scrollbars added & control structure screated

fixed typo in eqT's URI

CGLocateInductive patched

added the support for the "Locate Inductive Principles" query

* removed wrong unref

* added test .html file for mozilla plugin

* a few adjustments and debugging messages added
* works as a component in mozilla

Closed induction cases are now pointers to the acontext/conclusion ==>
they are now perforated correctly.

* added first version of persist stream implementation (not yet working)
* added test for property bag (read-only for now)

"proof of X" closed mactions were not selectable

1. folded maction are now selectable
2. metavariable occurrences are now displayed together with their
   substitution (to be improved)
3. the hypothesis in the metasenv are now displayed in the right order

* mime type updated

- support for comments added in mathql_db_map.txt

Unuseful id removed from hypothesis.

- information about the database map added in whatsnew.html
- spell checked

Eta fixing for MTCases added (that meant to recursively pass around the
context).

All the ids are now generated by gen_id. (Some of them were previously based
on the acic ids).

* quite a lot of patches in the building stuff

new links added

Added method FalseInd

Added method "FalseInd".

Prefixes introduced for the generated ids/xrefs. Example:
 "proof:" for proofs
 "decl:"  for declarations
 ...

- the mathql interpreter is not helm-dependent any more
- fixed a bug in the "match conclusion" query of the search engine
- gTopLevel/Makefile improved

Spurious files removed.

"(" moved from Mtext to Mo. Spaces removed.

Added method AndInd.

Added Method "exists".

Few modif in eta-fixing.

Missing xref for conjectures.

mathvariant=normal for all the proof ;-)

background (deprecated) ==> mathbackground

Bug fixed: it could have happened that the tree structured becomes scrambled
by the highlighting operation.

use OCAMLFIND variable instead of "ocamlfind" directly

- severe bug fixing
- implementation of two functions to highlight/dim set of nodes given
  their xref. [used to highlight/dim the current goal]

Highlighting of changed parts.

URIs of inductive types and constructors fixed.

Lemma generated wrong URIs (again). Fixed.

Complete beta reduction added to avoid strange case of deep beta-redexes
in the expected types of application heads.

Exact handled in a better way (no more "NO PROOFS").

The name of TD proofs was erroneously always set to previous.

Improved management of conclusions, to avoid repetitions.
Some problems of xrefs have been fixed.

- better handling of proof expansion/contraction
- helm:xref added in most places

- Lemma added to the list of proof arguments
- Lemma used for Const, MutConst and Var in Apply arguments
- atomization of complex proofs is now performed also in tactics different
  from Apply

Debugging stuff changed.

"Final" commit that patches termViewer while still enabling XML Diffing.
Awesome performances!

- selection attribute of maction is now explicitly generated
- all the conjectures are now put in a table to avoid too many
  changes that make Xml Diffing difficult.

Previous commit was erroneous and dit not compile.
Fixed.

Debugging code inserted bug in the code ;-)

XmlDiff-ing of DOM trees implemented.
SPECIAL FEATURE: the selection attribute of mactions are not patched.

1. Modificiations due to the change ot K.Aux
2. Assert false on Lambda with no name removed. Who generates them?

The Aux argument of conclude is now of type string (used to be int).
Case Fixed.

Interface change: only cobj2obj is exposed.

Flattening application contexts uncorrectly changed the proof ids.

** UNTESTED **
Fix and CoFix are now handled "correctly" ;-)

We do not compute inner-types for the metasenv ==> we handle it in a particular
way, always generating `Declaration and `Definition (instead of `Hypothesis and
`Proof when the sort is Prop).

Rendering of current proofs completed.

Reindenting.

proof2cic now uses Deannotate.deannoate_term instead of having an input
parameter.