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

some definitions about subsets

Error messages improvement.

Less verbose error messages (= substitution applied everywhere, terms pretty
printed in their context) are now printed by default.
There is a flag in cicUnification.ml to set the error messages to the
verbose mode.

Wrong reported error message fixed.

More information is now printed when reporting errors.

Typo fixed.

Disambiguation errors are no longer thrown away. They are now collected
and presented (in a not understandable way) to the user.

some renaming

Coercions are now inserted also around the sources of lambda abstractions.

more work for coercions

fix

fixed coercions undo

added debug items for enabling/disabling pretty printing notation completely

added support for enabling/disabling (pretty printing) notation

fix for coercions

Incredible bug fixed: coercions were computed and then partially thrown away
during eat_prods!

some more on tinycals

added more on tinycals

Improvement/bug fix: rewriting in the hypothesis used to simplify the
new hypothesis. This is no longer done.

...

New test for parallel rewriting in the hypotheses and in the conclusion.

Comments changed/removed.

"Parallel" rewriting in a list of hypothesis and in the conclusion is now
allowed.

Major code semplification and improvement:
 1. the proof term generated used to have a (Hletin) ...
    Now it has a (H) ...
 2. the code has been greatly simplified by renaming the old variable
    first and doing a letin later; I used to do the letin first and
    rename the new variable at the end

aded a prototype of chtting aboit tacticals

filled disambiguation algorithm section

First draft implementation of rewriting in an hypothesis.
Highly incomplete. Fails randomly if the pattern is not one the tactic is able
to cope with.

New tactic rename (for now for internal usage only).

matita.tex

followed kluwer guidelines