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.

The last commit about coercions disactivated localization of errors for
eat_prods. Localization restored.

since the moo content is not OK... we need an hack.

Big commit to let Ferruccio try the merge_coercion patch.

1) allowed :> syntax in record to specify that a field is a coercion
   (and it will be used (if needed) in defining the following projections)
2) minor cleanup in CicUtil.is_metaclosed
3) added library_objects.reset_defaults() (used in MatitaSync.init())
4) added MatitaSync.init() that is the only way to obtain an initial matita
   status
5) CoercDb is only accessed by CoercGraph
6) insert_coercion flag added to the refiner (and removed the use_coercion flag
   from CoercDb). Coercions are always available, the refiner will eventually
   insert them
7) CicRefiner now packs coercions with the avoid_double_coercion function
8) GrafiteAstPp is now "more" in sync and dump_moo seems to work again
9) LibrarySync has a merge_coercions function that calls on
   `Generated && not(is_coercion) objects. I hope it is enough (calling it
   on every objects shlows down a bit
10)MatitaScript now calls MatitaSync.init() on reset

TODO: - remove CoercGraph.remove_coercion from add_single_obj
      - find a place for CoercGraph.add_coercion used in generate_projections

Big commit to let Ferruccio try the merge_coercion patch.

1) allowed :> syntax in record to specify that a field is a coercion
   (and it will be used (if needed) in defining the following projections)
2) minor cleanup in CicUtil.is_metaclosed
3) added library_objects.reset_defaults() (used in MatitaSync.init())
4) added MatitaSync.init() that is the only way to obtain an initial matita    status
5) CoercDb is only accessed by CoercGraph
6) insert_coercion flag added to the refiner (and removed the use_coercion flag    from CoercDb). Coercions are always available, the refiner will eventually    insert them
7) CicRefiner now packs coercions with the avoid_double_coercion function
8) GrafiteAstPp is now "more" in sync and dump_moo seems to work again
9) LibrarySync has a merge_coercions function that calls on
   `Generated && not(is_coercion) objects. I hope it is enough (calling it
   on every objects shlows down a bit
10)MatitaScript now calls MatitaSync.init() on reset

TODO: - remove CoercGraph.remove_coercion from add_single_obj
      - find a place for CoercGraph.add_coercion used in generate_projections

bugfixes:
- added missing Makefile dep for saturate
- ported to new CicNotation2 module
- implemented interactive_user_uri_choice callback

Typos.

Minor changes.