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.

Naming convention.

better output from main_demod_equalities

added function term_of_equality to re-build the Cic.term from an equality

eval_from_stream_greedy finally got rid of!

removed original equalities from the output of main_demod_equalities

1. Several files in grafite that should be in grafite_parser moved there.
2. grafiteEngine is now generalized over the function baseuri_of_script
   (that associates the baseuri to a .ma file). This function is used to
   execute the Include statement. However, it seems to me that this shows
   a problem in the architecture (since the only possible implementation of
   the function involves using the grafie_parser right now).

Modified Files in ocaml:
METAS/meta.helm-grafite_parser.src grafite/.depend
grafite/Makefile grafite/cicNotation.ml
grafite/cicNotation.mli grafite2/disambiguatePp.ml
grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml
grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml
grafite2/grafiteMisc.mli grafite_parser/.depend
grafite_parser/Makefile
Modified Files in matita:
        matitaEngine.ml matitaEngine.mli matitaGui.ml matitaInit.ml
        matitaScript.ml matitacLib.ml matitaclean.ml matitadep.ml
Added Files in ocaml:
grafite_parser/cicNotation2.ml grafite_parser/cicNotation2.mli
grafite_parser/grafiteParser.ml
grafite_parser/grafiteParser.mli
grafite_parser/grafiteParserMisc.ml
grafite_parser/grafiteParserMisc.mli
grafite_parser/print_grammar.ml grafite_parser/test_dep.ml
grafite_parser/test_parser.ml
Removed Files in ocaml:
grafite/grafiteParser.ml grafite/grafiteParser.mli
grafite/print_grammar.ml grafite/test_dep.ml
grafite/test_parser.ml

1. Several files in grafite that should be in grafite_parser moved there.
2. grafiteEngine is now generalized over the function baseuri_of_script
   (that associates the baseuri to a .ma file). This function is used to
   execute the Include statement. However, it seems to me that this shows
   a problem in the architecture (since the only possible implementation of
   the function involves using the grafie_parser right now).

Modified Files in ocaml:
        METAS/meta.helm-grafite_parser.src grafite/.depend
        grafite/Makefile grafite/cicNotation.ml
        grafite/cicNotation.mli grafite2/disambiguatePp.ml
        grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml
        grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml
        grafite2/grafiteMisc.mli grafite_parser/.depend
        grafite_parser/Makefile
Modified Files in matita:
        matitaEngine.ml matitaEngine.mli matitaGui.ml matitaInit.ml
        matitaScript.ml matitacLib.ml matitaclean.ml matitadep.ml
Added Files in ocaml:
        grafite_parser/cicNotation2.ml grafite_parser/cicNotation2.mli
        grafite_parser/grafiteParser.ml
        grafite_parser/grafiteParser.mli
        grafite_parser/grafiteParserMisc.ml
        grafite_parser/grafiteParserMisc.mli
        grafite_parser/print_grammar.ml grafite_parser/test_dep.ml
        grafite_parser/test_parser.ml
Removed Files in ocaml:
        grafite/grafiteParser.ml grafite/grafiteParser.mli
        grafite/print_grammar.ml grafite/test_dep.ml
        grafite/test_parser.ml

removed some debug messages

added  function saturate_equations that tries to infer as many equations as possible within the time limit

Minor changes.

removed from repository spurious object files

Added a new section on the logical library.

metadata are no longer stored in .moo files.
They are now stored (and retrieved) in .metadata files if -nodb is set.
In this way the "library" library no longer depends on "content_pres"

1. metadata are no longer stored in .moo files.
   They are now stored (and retrieved) in .metadata files if -nodb is set.
   In this way the "library" library no longer depends on "content_pres"
2. removed files in grafite_parser that were commited by mistake

moved (and hence exported) uri rehashing functions on terms and objects to CicUtil

1. matitaEngine splitted into disambiguation (now in grafite_parser) and
   in evaluation (now in grafite2)
2. .moo files are now grafite ASTs at the CIC level; they used to be at the
   content (or even presentation?) level
3. coq.ma is no longer a special file; added "-I .." in tests to make them
   include coq.ma

Modified Files in ocaml:
        Makefile.in grafite/grafiteAst.ml grafite/grafiteAstPp.ml
        grafite/grafiteAstPp.mli grafite/grafiteMarshal.ml
        grafite/grafiteMarshal.mli grafite/grafiteParser.ml
        grafite/grafiteParser.mli library/libraryClean.ml
Modified Files in matita:
        .depend Makefile.in configure.ac coq.ma dump_moo.ml matita.ml
        matitaEngine.ml matitaEngine.mli matitaExcPp.ml
        matitaGtkMisc.ml matitaGui.ml matitaGuiTypes.mli
        matitaMathView.ml matitaMisc.ml matitaMisc.mli matitaScript.ml
        matitaScript.mli matitaTypes.ml matitaTypes.mli matitacLib.ml
        matitaclean.ml matitadep.ml tests/Makefile
Added Files in ocaml:
        METAS/meta.helm-grafite2.src
        METAS/meta.helm-grafite_parser.src grafite2/.cvsignore
        grafite2/.depend grafite2/Makefile 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/.cvsignore
        grafite_parser/.depend grafite_parser/Makefile
        grafite_parser/grafiteDisambiguate.cmi
        grafite_parser/grafiteDisambiguate.cmo
        grafite_parser/grafiteDisambiguate.cmx
        grafite_parser/grafiteDisambiguate.ml
        grafite_parser/grafiteDisambiguate.mli
        grafite_parser/grafiteDisambiguate.o
        grafite_parser/grafite_parser.a
        grafite_parser/grafite_parser.cma
        grafite_parser/grafite_parser.cmxa
        grafite_parser/matitaDisambiguator.cmi
        grafite_parser/matitaDisambiguator.cmo
        grafite_parser/matitaDisambiguator.cmx
        grafite_parser/matitaDisambiguator.ml
        grafite_parser/matitaDisambiguator.mli
        grafite_parser/matitaDisambiguator.o
Removed Files in matita:
        disambiguatePp.ml disambiguatePp.mli matitaDisambiguator.ml
        matitaDisambiguator.mli matitaSync.ml matitaSync.mli

1. matitaEngine splitted into disambiguation (now in grafite_parser) and
   in evaluation (now in grafite2)
2. .moo files are now grafite ASTs at the CIC level; they used to be at the
   content (or even presentation?) level
3. coq.ma is no longer a special file; added "-I .." in tests to make them
   include coq.ma

Modified Files in ocaml:
  Makefile.in grafite/grafiteAst.ml grafite/grafiteAstPp.ml
  grafite/grafiteAstPp.mli grafite/grafiteMarshal.ml
  grafite/grafiteMarshal.mli grafite/grafiteParser.ml
  grafite/grafiteParser.mli library/libraryClean.ml
Modified Files in matita:
        .depend Makefile.in configure.ac coq.ma dump_moo.ml matita.ml
        matitaEngine.ml matitaEngine.mli matitaExcPp.ml
        matitaGtkMisc.ml matitaGui.ml matitaGuiTypes.mli
        matitaMathView.ml matitaMisc.ml matitaMisc.mli matitaScript.ml
        matitaScript.mli matitaTypes.ml matitaTypes.mli matitacLib.ml
        matitaclean.ml matitadep.ml tests/Makefile
Added Files in ocaml:
  METAS/meta.helm-grafite2.src
  METAS/meta.helm-grafite_parser.src grafite2/.cvsignore
  grafite2/.depend grafite2/Makefile 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/.cvsignore
  grafite_parser/.depend grafite_parser/Makefile
  grafite_parser/grafiteDisambiguate.cmi
  grafite_parser/grafiteDisambiguate.cmo
  grafite_parser/grafiteDisambiguate.cmx
  grafite_parser/grafiteDisambiguate.ml
  grafite_parser/grafiteDisambiguate.mli
  grafite_parser/grafiteDisambiguate.o
  grafite_parser/grafite_parser.a
  grafite_parser/grafite_parser.cma
  grafite_parser/grafite_parser.cmxa
  grafite_parser/matitaDisambiguator.cmi
  grafite_parser/matitaDisambiguator.cmo
  grafite_parser/matitaDisambiguator.cmx
  grafite_parser/matitaDisambiguator.ml
  grafite_parser/matitaDisambiguator.mli
  grafite_parser/matitaDisambiguator.o
Removed Files in matita:
        disambiguatePp.ml disambiguatePp.mli matitaDisambiguator.ml
        matitaDisambiguator.mli matitaSync.ml matitaSync.mli

it may happen that matitaclean (clean_baseuris) calls the remove function
without having added the objects first... so the hashtbl is empty...
asert fasle -> []

moved coercion to library (work in progress)

moved coercions away (work in progress)

coercGraph.ml* moved from cic_unification to library

Implicit aliases are now defined as all the aliases whose baseuri is the
baseuri of the current development. Much much cleaner.

nicer (but convertible) types

* Undo fixed.
* Minor code cleaning.

Terms parsed by notations were not localized.

improved disambiguation section

Generation of auxiliary lemmas for inductive types and records moved
from cic_proof_checking and matita to ocaml/library.

* Part of matita that used to deal with the library moved into ocaml/library
* cic_unification/coercDb.ml* ==> library/coercDb.ml*

Added a few bibliographic entries.

coa continued

* More error messages localized.
* Bug fixed: a few Uncertain became RefineFailure in my last commit(s).

More errors localized.

More error messages localized.

More aggressive politic for non localized terms: an assert false!

first part on disambiguation passes

added comment

DisambiguationError exceptions (that have locations inside) are now relocated
correctly after a (** comment *).