incomplete proof completed

typo fixed: simmetry ==> symmetry

incomplete proof terminated

qed missing

Bug fixed: when the final proof_status is not No_proof matitac returns -1.

added fullscreen menu item

integrated lablgtksourceview

cosmetic fix

- no longer build mathql per default
- moved cic_notation after cic_transformation

renamed

fix

F2 hides the tactics buttons bar

- new minor version
- rebuilt against today lablgtk2 CVS snapshot

ported to official (guessed) version of lablgtk2

better clean up on dist

moved the annoying debugging print to test

ported to lablgtk2 2.4.0+2005.06.13-1

ported to latest lablgtk2 snapshot (13/06/2005) in which Garrigue
applied my patch about *_skel

fix

added syntax hilight for temperino

removed prerr_endline

fix

error

moved to xmlPushParser

fixed error in comment

rewritten makefile and debian packaging: .deb ready!

added an 'a parameter to mpresentation type so that it and boxes could
be used in a mutual recursive fashoin (boxes inside mpresentation inside
boxes ...) needed by cic_notation

ocaml 3.08.3 commit

fixed segfault issue with matching bracket search

first checkin of debian stuff, something done, but still almost copy and
paste from lablgtkmathview

snapshort
- bound (hidden) function for creation of language from file
- bound find_matching_bracket
- changed license to LGPL

added_test

added records

added mk_rel

added records pp, ast and fixed a bug in match with only one branch

added record generation modules

added record generation module

The type of the left parameters of an inductive type can now be omitted.

Got rid of a few bugs.

Got rid of a few warnings.

Got rid of a few warnings.

an assert failure changed to an exception and a bit of code cleanupt

The user is no longer obliged to give the types for definitions.

integrated indexing.ml, breaks everything :-P (previous working version tagged PRE_INDEXING_1)

debugging to false

* (Head) beta reduction functions factorized
* the type inferred for a match both in the kernel and in the refiner
  are now beta reduced

More debugging infos.

...

unshare.ml*

Complete unsharing of terms.

- bound GtkSourceLanguagesManager (only get_lang..from_mime_type)

snaphot
- better creation of GtkSourceView (using C constructor)
- bound GtkSourceLanguage
- preliminary binding of GtkSourceLanguagesManager

head_beta_reduce used to create applications of applications. Fixed.
head_beta_reduce renamed to beta_reduce (since it performs full beta reduction).

...

added source_view ?text constructor parameter

test file

load "test.txt" and show it in a scrolled win

snapshot
- implemented many methods of GtkSourceBuffer
- fixed creation of GtkSourceView (no longer assert failure on undo)

prima implementazione di demodulate, superposition_left e superposition_right
con gli "indici"...

cambiato il tipo equality, aggiunto l'ordinamento tra left e right

...

test_instance.ma moved to interactive/ (whose tests are not executed for
regression testing)

intro ==> intros

Error message improved.

Now CicMetaSubst.delift_rels restricts the Metas when a failure is faced.
This closes yet another bug in the inference of the outtype for matches.

No more explicit types for the branches of the matches: all the bugs
preventing automatic type inference have been fixed.

snapshot
- almost fully bound SourceView
- started binding of SourceBuffer

CicSubstitution.delift ==> CicMetaSubst.delift_rels
(since it will need to restrict metavariables in case of Rel capture)

lablgtksourceview: first checkin, almost nothing bound ...

Exception raised by delift changed:
Failure ==> DeliftingWouldCaptureAFreeVariable

Debugging code removed.

added debug item for coercion

added \n to "file saved" message

added whd before uri_of_term

removed debug prints

fixed remove_coercion

andrea.ma removed (superseded by match.ma)

Updated to the new syntax for match.

simplified cicBrowser: whelp bar is now always visible

- handles about:* uris in cicBrowser
- added comboboxentry in cicBrowser (still ugly ...)

fixed history handling: now both "home" and link reached via href are
correctly stored and remembered in history

rewritten cicBrowser handling of uri text entry, still some issued with browser
history

The type of a top-level "let rec" can be optional.

Let's try to make the "let rec" construct infer its arguments.

Syntax for top-level "let rec" fixed.

Using the lighter syntax for "let recs".

Using the top-level syntax for let-rec definitions.

The file is now well formed.

New syntax (again) for let rec binders:
let rec f x y (z,w:T) h (c:T) = ...

New lighter syntax for "let rec".

Bug fixed: a symbol must be formed of just one (unicode) character.

Query results were erroneously tagged as directories.

1. syntax of match changed
2. syntax of the bindings of "let rec" made lighter

Yet another bug fixed in the inference of the outtype for match: convertibility
was used in place of unification, making type inference much less powerful
in several useful cases.

The getter maps are now dumped also if matitac exits abruptly.

Added new target "make tests" for regression testing.

Fixed a few bugs in the inference of the outtype for a match.
In particular the instances of the left parameter that occur in the
outtype were not lifted properly because of the abstractions that correspond
to the right parameters.

Fixed inference of outtype for match when the inductive type has left and/or
right parameters.

Harder test (with empty inductive types and left and right arguments to
inductive types). It does not compile yet.

More informative error message.