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

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