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 *).

1. Bug fixed: compilation of "let corec" to a simple CoFix without a surrounding
   let...in was bugged (because of a missing delifting). Fixed.
2. Localization is no longer lost in the body of a "let rec" or a "let corec"

removed deadcode / fixed typos (thanks to ocaml 3.09)

removed dead code (thanks to ocaml 3.09)

crosso compatibility patch which enable building both with ocaml 3.08 and 3.09

ocaml 3.09 transition

* wrong comments removed
* relocalization of refined terms is now performed for every refined term

Refinement bug fixed. The outtype was not refined if it was an Implicit.

coimplication (continued)
complete overlap algebras (started)

Debugging code removed.

Bug fixed: an unrefined term was passed around while checking explicit named
substitutions.

Experimental localization of errors during refinement and disambiguation.

the coimplication connective (start)

Module CicHash (hash-tables over CIC terms based on physical equality) moved
into Cic.

s/0c2/0c2a/ in .install

...

Non exhaustive match fixed.

Bug fixed: removal of .__log was not always attempted.

use empty universe in the mono alias phases

bugfix: removed unneeded No_choices exception
bugfix: avoid looking in the library when explecitely asked not to do so

Confronto con Coq.

minor changes

labels

...

...

deps

More on the presentation.

fix

added missing deps

...

build paper per default

dependency graphs

notation intro

added tinycals and patterns subsections

changed META dependency
- disambiguation should (and actually does) depend only on acic_content
- paramodulation does not need disambiguation! (except for a test)

Unused file removed.

Reshaped structure of ocaml/ libraries, matita changed accordingly.
Verbose list of the changes:
  Modified Files:
  Makefile.in METAS/meta.helm-cic_disambiguation.src
  cic_disambiguation/.depend cic_disambiguation/Makefile
  cic_disambiguation/disambiguate.ml
  cic_disambiguation/disambiguate.mli
  cic_disambiguation/disambiguateChoices.ml
  cic_disambiguation/disambiguateTypes.ml
  cic_disambiguation/disambiguateTypes.mli extlib/.depend
  extlib/Makefile xml/xml.ml xml/xml.mli
  Added Files:
  METAS/meta.helm-acic_content.src METAS/meta.helm-cic_acic.src
  METAS/meta.helm-content_pres.src METAS/meta.helm-grafite.src
  METAS/meta.helm-hgdome.src acic_content/.cvsignore
  acic_content/.depend acic_content/Makefile
  acic_content/acic2astMatcher.ml
  acic_content/acic2astMatcher.mli acic_content/acic2content.ml
  acic_content/acic2content.mli acic_content/cicNotationEnv.ml
  acic_content/cicNotationEnv.mli acic_content/cicNotationPp.ml
  acic_content/cicNotationPp.mli acic_content/cicNotationPt.ml
  acic_content/cicNotationUtil.ml
  acic_content/cicNotationUtil.mli acic_content/content.ml
  acic_content/content.mli acic_content/content2cic.ml
  acic_content/content2cic.mli acic_content/contentPp.ml
  acic_content/contentPp.mli acic_content/termAcicContent.ml
  acic_content/termAcicContent.mli cic_acic/.cvsignore
  cic_acic/.depend cic_acic/Makefile cic_acic/cic2Xml.ml
  cic_acic/cic2Xml.mli cic_acic/cic2acic.ml
  cic_acic/cic2acic.mli cic_acic/doubleTypeInference.ml
  cic_acic/doubleTypeInference.mli cic_acic/eta_fixing.ml
  cic_acic/eta_fixing.mli content_pres/.cvsignore
  content_pres/.depend content_pres/Makefile content_pres/box.ml
  content_pres/box.mli content_pres/boxPp.ml
  content_pres/boxPp.mli content_pres/cicNotationLexer.ml
  content_pres/cicNotationLexer.mli
  content_pres/cicNotationParser.ml
  content_pres/cicNotationParser.mli
  content_pres/cicNotationPres.ml
  content_pres/cicNotationPres.mli content_pres/content2pres.ml
  content_pres/content2pres.mli
  content_pres/content2presMatcher.ml
  content_pres/content2presMatcher.mli
  content_pres/mpresentation.ml content_pres/mpresentation.mli
  content_pres/renderingAttrs.ml content_pres/renderingAttrs.mli
  content_pres/sequent2pres.ml content_pres/sequent2pres.mli
  content_pres/termContentPres.ml
  content_pres/termContentPres.mli content_pres/test_lexer.ml
  extlib/patternMatcher.ml extlib/patternMatcher.mli
  grafite/.cvsignore grafite/.depend grafite/Makefile
  grafite/cicNotation.ml grafite/cicNotation.mli
  grafite/grafiteAst.ml grafite/grafiteAstPp.ml
  grafite/grafiteAstPp.mli grafite/grafiteParser.ml
  grafite/grafiteParser.mli grafite/print_grammar.ml
  grafite/test_dep.ml grafite/test_parser.ml hgdome/.cvsignore
  hgdome/.depend hgdome/Makefile hgdome/domMisc.ml
  hgdome/domMisc.mli hgdome/xml2Gdome.ml hgdome/xml2Gdome.mli
  Removed Files:
  METAS/meta.helm-cic_notation.src METAS/meta.helm-cic_omdoc.src
  METAS/meta.helm-cic_transformations.src
  cic_disambiguation/disambiguatePp.ml
  cic_disambiguation/disambiguatePp.mli cic_notation/.cvsignore
  cic_notation/.depend cic_notation/Makefile cic_notation/TODO
  cic_notation/box.ml cic_notation/box.mli cic_notation/boxPp.ml
  cic_notation/boxPp.mli cic_notation/cicNotation.ml
  cic_notation/cicNotation.mli cic_notation/cicNotationEnv.ml
  cic_notation/cicNotationEnv.mli cic_notation/cicNotationFwd.ml
  cic_notation/cicNotationFwd.mli
  cic_notation/cicNotationLexer.ml
  cic_notation/cicNotationLexer.mli
  cic_notation/cicNotationMatcher.ml
  cic_notation/cicNotationMatcher.mli
  cic_notation/cicNotationParser.expanded.ml
  cic_notation/cicNotationParser.ml
  cic_notation/cicNotationParser.mli
  cic_notation/cicNotationPp.ml cic_notation/cicNotationPp.mli
  cic_notation/cicNotationPres.ml
  cic_notation/cicNotationPres.mli cic_notation/cicNotationPt.ml
  cic_notation/cicNotationRew.ml cic_notation/cicNotationRew.mli
  cic_notation/cicNotationTag.ml cic_notation/cicNotationTag.mli
  cic_notation/cicNotationUtil.ml
  cic_notation/cicNotationUtil.mli cic_notation/grafiteAst.ml
  cic_notation/grafiteAstPp.ml cic_notation/grafiteAstPp.mli
  cic_notation/grafiteParser.ml cic_notation/grafiteParser.mli
  cic_notation/mpresentation.ml cic_notation/mpresentation.mli
  cic_notation/print_grammar.ml cic_notation/renderingAttrs.ml
  cic_notation/renderingAttrs.mli cic_notation/test_dep.ml
  cic_notation/test_lexer.ml cic_notation/test_parser.conf.xml
  cic_notation/test_parser.ml cic_notation/doc/.cvsignore
  cic_notation/doc/Makefile cic_notation/doc/body.tex
  cic_notation/doc/infernce.sty cic_notation/doc/ligature.sty
  cic_notation/doc/main.tex cic_notation/doc/manfnt.sty
  cic_notation/doc/reserved.sty cic_notation/doc/samples.ma
  cic_notation/doc/semantic.sty cic_notation/doc/shrthand.sty
  cic_notation/doc/tdiagram.sty cic_omdoc/.cvsignore
  cic_omdoc/.depend cic_omdoc/Makefile cic_omdoc/cic2acic.ml
  cic_omdoc/cic2acic.mli cic_omdoc/cic2content.ml
  cic_omdoc/cic2content.mli cic_omdoc/content.ml
  cic_omdoc/content.mli cic_omdoc/content2cic.ml
  cic_omdoc/content2cic.mli cic_omdoc/contentPp.ml
  cic_omdoc/contentPp.mli cic_omdoc/doubleTypeInference.ml
  cic_omdoc/doubleTypeInference.mli cic_omdoc/eta_fixing.ml
  cic_omdoc/eta_fixing.mli cic_transformations/.cvsignore
  cic_transformations/.depend cic_transformations/Makefile
  cic_transformations/applyTransformation.ml
  cic_transformations/applyTransformation.mli
  cic_transformations/cic2Xml.ml cic_transformations/cic2Xml.mli
  cic_transformations/content2pres.ml
  cic_transformations/content2pres.mli
  cic_transformations/domMisc.ml cic_transformations/domMisc.mli
  cic_transformations/sequent2pres.ml
  cic_transformations/sequent2pres.mli
  cic_transformations/xml2Gdome.ml
  cic_transformations/xml2Gdome.mli

Reshaped structure of ocaml/ libraries.
Verbose list of the changes:
  Modified Files:
  Makefile.in METAS/meta.helm-cic_disambiguation.src
  cic_disambiguation/.depend cic_disambiguation/Makefile
  cic_disambiguation/disambiguate.ml
  cic_disambiguation/disambiguate.mli
  cic_disambiguation/disambiguateChoices.ml
  cic_disambiguation/disambiguateTypes.ml
  cic_disambiguation/disambiguateTypes.mli extlib/.depend
  extlib/Makefile xml/xml.ml xml/xml.mli
  Added Files:
  METAS/meta.helm-acic_content.src METAS/meta.helm-cic_acic.src
  METAS/meta.helm-content_pres.src METAS/meta.helm-grafite.src
  METAS/meta.helm-hgdome.src acic_content/.cvsignore
  acic_content/.depend acic_content/Makefile
  acic_content/acic2astMatcher.ml
  acic_content/acic2astMatcher.mli acic_content/acic2content.ml
  acic_content/acic2content.mli acic_content/cicNotationEnv.ml
  acic_content/cicNotationEnv.mli acic_content/cicNotationPp.ml
  acic_content/cicNotationPp.mli acic_content/cicNotationPt.ml
  acic_content/cicNotationUtil.ml
  acic_content/cicNotationUtil.mli acic_content/content.ml
  acic_content/content.mli acic_content/content2cic.ml
  acic_content/content2cic.mli acic_content/contentPp.ml
  acic_content/contentPp.mli acic_content/termAcicContent.ml
  acic_content/termAcicContent.mli cic_acic/.cvsignore
  cic_acic/.depend cic_acic/Makefile cic_acic/cic2Xml.ml
  cic_acic/cic2Xml.mli cic_acic/cic2acic.ml
  cic_acic/cic2acic.mli cic_acic/doubleTypeInference.ml
  cic_acic/doubleTypeInference.mli cic_acic/eta_fixing.ml
  cic_acic/eta_fixing.mli content_pres/.cvsignore
  content_pres/.depend content_pres/Makefile content_pres/box.ml
  content_pres/box.mli content_pres/boxPp.ml
  content_pres/boxPp.mli content_pres/cicNotationLexer.ml
  content_pres/cicNotationLexer.mli
  content_pres/cicNotationParser.ml
  content_pres/cicNotationParser.mli
  content_pres/cicNotationPres.ml
  content_pres/cicNotationPres.mli content_pres/content2pres.ml
  content_pres/content2pres.mli
  content_pres/content2presMatcher.ml
  content_pres/content2presMatcher.mli
  content_pres/mpresentation.ml content_pres/mpresentation.mli
  content_pres/renderingAttrs.ml content_pres/renderingAttrs.mli
  content_pres/sequent2pres.ml content_pres/sequent2pres.mli
  content_pres/termContentPres.ml
  content_pres/termContentPres.mli content_pres/test_lexer.ml
  extlib/patternMatcher.ml extlib/patternMatcher.mli
  grafite/.cvsignore grafite/.depend grafite/Makefile
  grafite/cicNotation.ml grafite/cicNotation.mli
  grafite/grafiteAst.ml grafite/grafiteAstPp.ml
  grafite/grafiteAstPp.mli grafite/grafiteParser.ml
  grafite/grafiteParser.mli grafite/print_grammar.ml
  grafite/test_dep.ml grafite/test_parser.ml hgdome/.cvsignore
  hgdome/.depend hgdome/Makefile hgdome/domMisc.ml
  hgdome/domMisc.mli hgdome/xml2Gdome.ml hgdome/xml2Gdome.mli
  Removed Files:
  METAS/meta.helm-cic_notation.src METAS/meta.helm-cic_omdoc.src
  METAS/meta.helm-cic_transformations.src
  cic_disambiguation/disambiguatePp.ml
  cic_disambiguation/disambiguatePp.mli cic_notation/.cvsignore
  cic_notation/.depend cic_notation/Makefile cic_notation/TODO
  cic_notation/box.ml cic_notation/box.mli cic_notation/boxPp.ml
  cic_notation/boxPp.mli cic_notation/cicNotation.ml
  cic_notation/cicNotation.mli cic_notation/cicNotationEnv.ml
  cic_notation/cicNotationEnv.mli cic_notation/cicNotationFwd.ml
  cic_notation/cicNotationFwd.mli
  cic_notation/cicNotationLexer.ml
  cic_notation/cicNotationLexer.mli
  cic_notation/cicNotationMatcher.ml
  cic_notation/cicNotationMatcher.mli
  cic_notation/cicNotationParser.expanded.ml
  cic_notation/cicNotationParser.ml
  cic_notation/cicNotationParser.mli
  cic_notation/cicNotationPp.ml cic_notation/cicNotationPp.mli
  cic_notation/cicNotationPres.ml
  cic_notation/cicNotationPres.mli cic_notation/cicNotationPt.ml
  cic_notation/cicNotationRew.ml cic_notation/cicNotationRew.mli
  cic_notation/cicNotationTag.ml cic_notation/cicNotationTag.mli
  cic_notation/cicNotationUtil.ml
  cic_notation/cicNotationUtil.mli cic_notation/grafiteAst.ml
  cic_notation/grafiteAstPp.ml cic_notation/grafiteAstPp.mli
  cic_notation/grafiteParser.ml cic_notation/grafiteParser.mli
  cic_notation/mpresentation.ml cic_notation/mpresentation.mli
  cic_notation/print_grammar.ml cic_notation/renderingAttrs.ml
  cic_notation/renderingAttrs.mli cic_notation/test_dep.ml
  cic_notation/test_lexer.ml cic_notation/test_parser.conf.xml
  cic_notation/test_parser.ml cic_notation/doc/.cvsignore
  cic_notation/doc/Makefile cic_notation/doc/body.tex
  cic_notation/doc/infernce.sty cic_notation/doc/ligature.sty
  cic_notation/doc/main.tex cic_notation/doc/manfnt.sty
  cic_notation/doc/reserved.sty cic_notation/doc/samples.ma
  cic_notation/doc/semantic.sty cic_notation/doc/shrthand.sty
  cic_notation/doc/tdiagram.sty cic_omdoc/.cvsignore
  cic_omdoc/.depend cic_omdoc/Makefile cic_omdoc/cic2acic.ml
  cic_omdoc/cic2acic.mli cic_omdoc/cic2content.ml
  cic_omdoc/cic2content.mli cic_omdoc/content.ml
  cic_omdoc/content.mli cic_omdoc/content2cic.ml
  cic_omdoc/content2cic.mli cic_omdoc/contentPp.ml
  cic_omdoc/contentPp.mli cic_omdoc/doubleTypeInference.ml
  cic_omdoc/doubleTypeInference.mli cic_omdoc/eta_fixing.ml
  cic_omdoc/eta_fixing.mli cic_transformations/.cvsignore
  cic_transformations/.depend cic_transformations/Makefile
  cic_transformations/applyTransformation.ml
  cic_transformations/applyTransformation.mli
  cic_transformations/cic2Xml.ml cic_transformations/cic2Xml.mli
  cic_transformations/content2pres.ml
  cic_transformations/content2pres.mli
  cic_transformations/domMisc.ml cic_transformations/domMisc.mli
  cic_transformations/sequent2pres.ml
  cic_transformations/sequent2pres.mli
  cic_transformations/xml2Gdome.ml
  cic_transformations/xml2Gdome.mli

...

Da capo (matita2.tex).

split non-logic level of whelp away from metadataQuery to a new module

added missing dependency

removed the need of REQUIRES in libraries Makefile, they are now queried from the corresponding META

bugfix: libraries.ps works again

prose

minimal introduction

New implementation for localized exceptions.

* New implementation of localized exceptions
* Localized exceptions moved into the extlib

...

ocaml 3.09 transition

More on accessibility.

ocaml 3.09 transition

ocaml 3.09 transition

0.7.2 version (ancient)

- more resilient to proof checking failures during pretty printing
- do not compute inner types for sequents

support pretty printing of Cic.Implicit

bugfix: return unshared sequent when applying cic -> mathml transformations so that paste work again

Debugging code commented out.

Error messages improved.

"Localization" of error messages for eat_prods and applications.

Less verbose error messages.

Last details.

Proof using function induction terminated. It's really gorgeous.

Lost of redundant typing hints removed from the functional induction term.

New proof based on an hand-made functional induction.

Useful lemma added.

Invariant no longer true (since when?)

More informative error messages.

split body away to ease inclusion from elsewhere

split to easy inclusion

typo

internal quantification fixed

fixed URI regexp so that URIs containing '-' are allowed

"let rec f = ... in f l" used to be compiled incorrectly
(without checking if f occurs in l and without delifting l!!!)

theorems about equality in classes