Dead code clean-up.

Dead code for packing/unpacking (usually just a big hack) commented out
(hopefully forever).

Dead code clean-up.

added decrease and increase font size fantafeature

added utility to dump some tables of the db on mowgli
(useful to export metadata to laptops)

matita.conf.xml added

removed again (I added it by error :-(

* parsing errors in tests were not detected and the rest of the file was
  ignored!!!! Tests fixed
* a few interactive tests moved to tests/interactive to avoid regression
  testing over them (for now...)

DTD for attributes revised.
New syntax:
 <attributes>
  <class type="..">
   ...
  </class>
  <generated />
 </attributes>
where the ... are the arguments of the class and the class and generated
elements are optional. For the "elim" class the only argument is the SORT.
For the "record" class the arguments are a list of <field name=".."/>

Syntax of <attributes>...</attributes> improved to allow arguments for
classes.

DTD for attributes revised.
New syntax:
 <attributes>
  <class type="..">
   ...
  </class>
  <generated />
 </attributes>
where the ... are the arguments of the class and the class and generated
elements are optional. For the "elim" class the only argument is the SORT.
For the "record" class the arguments are a list of <field name=".."/>

The `Record class now records also the name of the fields
(used to generate the projections)

a parser error is now logged as an error!

Bug fixed: parsing errors were ignored by matitac since the EOI was not
required to terminate the list of commands!

Bug fixed (that used to throw away a metasenv :-(

fix

renamed clientHTTP to http_getter_wget

we no longer use pxp

support for the new tactics lapply and fwd
used in forward reasoning

enable static linking of C stub code

version 0.7.1-1

- better printing of modifiers
- quit on window destroy

beginning of the tactics lapply and fwd
used to support forward reasoning

sync with new typecheck prototype (no more univ graph)

...

apply_tac used to calculate the type of the term before generalizing on explicit name subts

are_convertible on MutCase was no longer checking the match arguments
convertibility.

ported to latest registry interface

- support for multiple bindings of the same key, accessible via get_list
- changed get_opt interface so that marshallers/unmarshallers are needed
  instead of getters/setters

Refinement of CurrentProof did not check whether the type is a type.
As a consequence it was possible to do "theorem t: 0" :-)

Big commit and major code clean-up:
1. added a refine function for objects
2. added a disambiguation function for objects
3. MatitaEngine now uses the disambiguation function for objects
4. added CicTypeChecker.typecheck_obj to typecheck an object and add it
   to the environment

comments syntax changed

incomplete proof completed.

use META helm-registry package, load sample.xml and open Helm_registry

now something works...

* no more %% comments
* parsed comments must start with "(**b" where b is any blank
  and must be termianted by "*)"

No more %% comments.

parentheses allowed inside comments

test_lexer and test_parser compiled by default

uses XmlPushParser instead of PXP

finally we understood how to properly link ocaml bindings ....

fix

removed ocaml-pxp

hack to compile on gazelle

done two items

don't build pxp (no longer needed), cic_annotations (triassic dinosaur),
hbugs (coming soon ...)

removed dependencies on Pxp

removed dependency on cicPxpParser

uses XmlPushParser instead of Pxp for parsing getter resolve answer

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)