fix

reimplemented specific marshallars on top of generic HMarshal marshaller

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

added generic marshaller

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

fix

old files

fix

fix

removed old Makefile

fix

bench

__ files are removed

no more "completed in ."

Huge reorganization of matita and ocaml.

Modified Files in matita:
        .depend configure.ac matita.ml matitaEngine.ml
        matitaEngine.mli matitaExcPp.ml matitaGui.ml matitaGui.mli
        matitaInit.ml matitaInit.mli matitaMathView.ml matitaScript.ml
        matitaScript.mli matitacLib.ml matitaclean.ml matitadep.ml
Modified Files in ocaml:
.cvsignore Makefile.in clusters.dot daemons.dot patch_deps.sh
METAS/meta.helm-grafite.src METAS/meta.helm-grafite_parser.src
cic/cic.ml cic_disambiguation/disambiguate.ml
cic_disambiguation/disambiguateTypes.ml
cic_disambiguation/disambiguateTypes.mli extlib/hExtlib.ml
extlib/hExtlib.mli grafite/.depend grafite/Makefile
grafite/grafiteAst.ml grafite/grafiteAstPp.ml
grafite/grafiteAstPp.mli grafite/grafiteMarshal.ml
grafite2/.depend grafite2/Makefile grafite_parser/.depend
grafite_parser/Makefile grafite_parser/cicNotation2.ml
grafite_parser/cicNotation2.mli
grafite_parser/grafiteDisambiguate.ml
grafite_parser/grafiteDisambiguate.mli
grafite_parser/grafiteParser.ml
grafite_parser/grafiteParser.mli grafite_parser/test_dep.ml
grafite_parser/test_parser.ml library/libraryClean.ml
library/libraryMisc.ml library/libraryMisc.mli
library/libraryNoDb.ml library/libraryNoDb.mli
library/librarySync.ml tactics/.depend
tactics/equalityTactics.mli tactics/proofEngineHelpers.ml
tactics/proofEngineTypes.ml tactics/proofEngineTypes.mli
tactics/reductionTactics.mli tactics/tactics.mli
Added Files in ocaml:
METAS/meta.helm-grafite_engine.src METAS/meta.helm-lexicon.src
grafite_engine/.cvsignore grafite_engine/.depend
grafite_engine/Makefile grafite_engine/grafiteEngine.ml
grafite_engine/grafiteEngine.mli grafite_engine/grafiteMisc.ml
grafite_engine/grafiteMisc.mli grafite_engine/grafiteSync.ml
grafite_engine/grafiteSync.mli grafite_engine/grafiteTypes.ml
grafite_engine/grafiteTypes.mli
grafite_parser/dependenciesParser.ml
grafite_parser/dependenciesParser.mli
grafite_parser/grafiteDisambiguator.ml
grafite_parser/grafiteDisambiguator.mli lexicon/.cvsignore
lexicon/.depend lexicon/Makefile lexicon/cicNotation.ml
lexicon/cicNotation.mli lexicon/disambiguatePp.ml
lexicon/disambiguatePp.mli lexicon/lexiconAst.ml
lexicon/lexiconAstPp.ml lexicon/lexiconAstPp.mli
lexicon/lexiconEngine.ml lexicon/lexiconEngine.mli
lexicon/lexiconMarshal.ml lexicon/lexiconMarshal.mli
lexicon/lexiconSync.ml lexicon/lexiconSync.mli
Removed Files in ocaml:
METAS/meta.helm-grafite2.src grafite/cicNotation.ml
grafite/cicNotation.mli grafite2/disambiguatePp.ml
grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml
grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml
grafite2/grafiteMisc.mli grafite2/grafiteTypes.ml
grafite2/grafiteTypes.mli grafite2/matitaSync.ml
grafite2/matitaSync.mli grafite_parser/grafiteParserMisc.ml
grafite_parser/grafiteParserMisc.mli
grafite_parser/matitaDisambiguator.ml
grafite_parser/matitaDisambiguator.mli

Huge reorganization of matita and ocaml.

Modified Files in matita:
        .depend configure.ac matita.ml matitaEngine.ml
        matitaEngine.mli matitaExcPp.ml matitaGui.ml matitaGui.mli
        matitaInit.ml matitaInit.mli matitaMathView.ml matitaScript.ml
        matitaScript.mli matitacLib.ml matitaclean.ml matitadep.ml
Modified Files in ocaml:
        .cvsignore Makefile.in clusters.dot daemons.dot patch_deps.sh
        METAS/meta.helm-grafite.src METAS/meta.helm-grafite_parser.src
        cic/cic.ml cic_disambiguation/disambiguate.ml
        cic_disambiguation/disambiguateTypes.ml
        cic_disambiguation/disambiguateTypes.mli extlib/hExtlib.ml
        extlib/hExtlib.mli grafite/.depend grafite/Makefile
        grafite/grafiteAst.ml grafite/grafiteAstPp.ml
        grafite/grafiteAstPp.mli grafite/grafiteMarshal.ml
        grafite2/.depend grafite2/Makefile grafite_parser/.depend
        grafite_parser/Makefile grafite_parser/cicNotation2.ml
        grafite_parser/cicNotation2.mli
        grafite_parser/grafiteDisambiguate.ml
        grafite_parser/grafiteDisambiguate.mli
        grafite_parser/grafiteParser.ml
        grafite_parser/grafiteParser.mli grafite_parser/test_dep.ml
        grafite_parser/test_parser.ml library/libraryClean.ml
        library/libraryMisc.ml library/libraryMisc.mli
        library/libraryNoDb.ml library/libraryNoDb.mli
        library/librarySync.ml tactics/.depend
        tactics/equalityTactics.mli tactics/proofEngineHelpers.ml
        tactics/proofEngineTypes.ml tactics/proofEngineTypes.mli
        tactics/reductionTactics.mli tactics/tactics.mli
Added Files in ocaml:
        METAS/meta.helm-grafite_engine.src METAS/meta.helm-lexicon.src
        grafite_engine/.cvsignore grafite_engine/.depend
        grafite_engine/Makefile grafite_engine/grafiteEngine.ml
        grafite_engine/grafiteEngine.mli grafite_engine/grafiteMisc.ml
        grafite_engine/grafiteMisc.mli grafite_engine/grafiteSync.ml
        grafite_engine/grafiteSync.mli grafite_engine/grafiteTypes.ml
        grafite_engine/grafiteTypes.mli
        grafite_parser/dependenciesParser.ml
        grafite_parser/dependenciesParser.mli
        grafite_parser/grafiteDisambiguator.ml
        grafite_parser/grafiteDisambiguator.mli lexicon/.cvsignore
        lexicon/.depend lexicon/Makefile lexicon/cicNotation.ml
        lexicon/cicNotation.mli lexicon/disambiguatePp.ml
        lexicon/disambiguatePp.mli lexicon/lexiconAst.ml
        lexicon/lexiconAstPp.ml lexicon/lexiconAstPp.mli
        lexicon/lexiconEngine.ml lexicon/lexiconEngine.mli
        lexicon/lexiconMarshal.ml lexicon/lexiconMarshal.mli
        lexicon/lexiconSync.ml lexicon/lexiconSync.mli
Removed Files in ocaml:
        METAS/meta.helm-grafite2.src grafite/cicNotation.ml
        grafite/cicNotation.mli grafite2/disambiguatePp.ml
        grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml
        grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml
        grafite2/grafiteMisc.mli grafite2/grafiteTypes.ml
        grafite2/grafiteTypes.mli grafite2/matitaSync.ml
        grafite2/matitaSync.mli grafite_parser/grafiteParserMisc.ml
        grafite_parser/grafiteParserMisc.mli
        grafite_parser/matitaDisambiguator.ml
        grafite_parser/matitaDisambiguator.mli

fixed cicbrowser.opt argv.(0)

bugfix: typo which implied using the wrong pattern

added ocamldep.opt checking

moved term indexing (in both discrimination and path tree forms) from paramodulation/ to cic/

Discrimination and trie removed.

upgraded dependency figures

removed spurious arrows from Matita

added discrimination tree

moved trie data-structure

libraries-ext.ps generation (dep graph with daemons and clusters)

regenerated

New tactic: inversion.
 - only first phase implemented (no cleaning)
  - code in inversion.ml to be improved/cleaned up

New tactic: inversion.
 - only first phase implemented (no cleaning)
 - code in inversion.ml to be improved/cleaned up

...

added -I ../.. (for coq.ma)

ignore generated images

added htaccess

rm .depend

added -I../..

one more try

aaaa

fix

...

added ensure_path_exists to save_moo

fix

...

fixed_names

fixed_names

added comment explaining the meaning of the return value of get_candidates

added comment explaining the meaning of the return value of find_matches

bugfix: tactic invocations from contextual menu no longer generate content out of sync wrt locked mark

added contextual menu to act over selected terms
work in progress: still bugged wrt the locked mark of matitaScript

coercion command now requires an uri

ported to new types in grafite*/

- coercion now requires an URI
- ported to new pattern type

abstracted pretty printers over inner pretty printing units (terms, lazy terms, and objects)

changed pattern datatype:
- now the goal_pattern (third component) is optional, instead of using Cic.Implicit without annotation to denote non-specified pattern
- now the patter is polymorph over terms and lazy terms

add to the ids_to_father_ids table entries from hypothesis roots to hypothesis ids

fix

fixed coercions

fixed undo support for coercions inside records

convert does not export xfc->png properly...

fix

fix

fix

added developers

fix

fix

first draft

Bug fixed: errors of phase 7 were no longer printed :-)

1. useless code (undebrujin) removed from disambiguate.ml
2. debrujin now takes a callback used for localization during refinemente :-|
3. localization of inductive types fixed

commented out some debugging prints

implemented copy/cut/paste/delete/pastePattern

ficed include and -I

More compact disambiguation errors.