]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agoadded developers
Enrico Tassi [Mon, 12 Dec 2005 11:14:26 +0000 (11:14 +0000)]
added developers

18 years agofix
Enrico Tassi [Mon, 12 Dec 2005 11:03:23 +0000 (11:03 +0000)]
fix

18 years agofix
Enrico Tassi [Mon, 12 Dec 2005 10:55:53 +0000 (10:55 +0000)]
fix

18 years agofirst draft
Enrico Tassi [Mon, 12 Dec 2005 10:53:44 +0000 (10:53 +0000)]
first draft

18 years agoBug fixed: errors of phase 7 were no longer printed :-)
Claudio Sacerdoti Coen [Fri, 9 Dec 2005 16:01:46 +0000 (16:01 +0000)]
Bug fixed: errors of phase 7 were no longer printed :-)

18 years ago1. useless code (undebrujin) removed from disambiguate.ml
Claudio Sacerdoti Coen [Fri, 9 Dec 2005 15:53:18 +0000 (15:53 +0000)]
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

18 years agocommented out some debugging prints
Stefano Zacchiroli [Fri, 9 Dec 2005 13:04:15 +0000 (13:04 +0000)]
commented out some debugging prints

18 years agoimplemented copy/cut/paste/delete/pastePattern
Stefano Zacchiroli [Fri, 9 Dec 2005 13:00:47 +0000 (13:00 +0000)]
implemented copy/cut/paste/delete/pastePattern

18 years agoficed include and -I
Enrico Tassi [Fri, 9 Dec 2005 10:52:50 +0000 (10:52 +0000)]
ficed include and -I

18 years agoMore compact disambiguation errors.
Claudio Sacerdoti Coen [Wed, 7 Dec 2005 19:00:25 +0000 (19:00 +0000)]
More compact disambiguation errors.

18 years agoThe last commit about coercions disactivated localization of errors for
Claudio Sacerdoti Coen [Wed, 7 Dec 2005 18:59:22 +0000 (18:59 +0000)]
The last commit about coercions disactivated localization of errors for
eat_prods. Localization restored.

18 years agosince the moo content is not OK... we need an hack.
Enrico Tassi [Wed, 7 Dec 2005 15:53:14 +0000 (15:53 +0000)]
since the moo content is not OK... we need an hack.

18 years agoBig commit to let Ferruccio try the merge_coercion patch.
Enrico Tassi [Wed, 7 Dec 2005 15:42:42 +0000 (15:42 +0000)]
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

18 years agoBig commit to let Ferruccio try the merge_coercion patch.
Enrico Tassi [Wed, 7 Dec 2005 15:42:37 +0000 (15:42 +0000)]
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

18 years agobugfixes:
Stefano Zacchiroli [Tue, 6 Dec 2005 15:19:25 +0000 (15:19 +0000)]
bugfixes:
- added missing Makefile dep for saturate
- ported to new CicNotation2 module
- implemented interactive_user_uri_choice callback

18 years agoTypos.
Andrea Asperti [Tue, 6 Dec 2005 12:01:00 +0000 (12:01 +0000)]
Typos.

18 years agoMinor changes.
Andrea Asperti [Tue, 6 Dec 2005 11:57:34 +0000 (11:57 +0000)]
Minor changes.

18 years agoNaming convention.
Andrea Asperti [Tue, 6 Dec 2005 11:36:15 +0000 (11:36 +0000)]
Naming convention.

18 years agobetter output from main_demod_equalities
Alberto Griggio [Mon, 5 Dec 2005 16:49:13 +0000 (16:49 +0000)]
better output from main_demod_equalities

18 years agoadded function term_of_equality to re-build the Cic.term from an equality
Alberto Griggio [Mon, 5 Dec 2005 16:48:44 +0000 (16:48 +0000)]
added function term_of_equality to re-build the Cic.term from an equality

18 years agoeval_from_stream_greedy finally got rid of!
Claudio Sacerdoti Coen [Mon, 5 Dec 2005 15:05:21 +0000 (15:05 +0000)]
eval_from_stream_greedy finally got rid of!

18 years agoremoved original equalities from the output of main_demod_equalities
Alberto Griggio [Mon, 5 Dec 2005 15:04:12 +0000 (15:04 +0000)]
removed original equalities from the output of main_demod_equalities

18 years ago1. Several files in grafite that should be in grafite_parser moved there.
Claudio Sacerdoti Coen [Mon, 5 Dec 2005 14:09:31 +0000 (14:09 +0000)]
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

18 years ago1. Several files in grafite that should be in grafite_parser moved there.
Claudio Sacerdoti Coen [Mon, 5 Dec 2005 14:09:29 +0000 (14:09 +0000)]
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

18 years agoremoved some debug messages
Alberto Griggio [Mon, 5 Dec 2005 12:32:27 +0000 (12:32 +0000)]
removed some debug messages

18 years agoadded function saturate_equations that tries to infer as many equations as possible...
Alberto Griggio [Mon, 5 Dec 2005 12:32:06 +0000 (12:32 +0000)]
added  function saturate_equations that tries to infer as many equations as possible within the time limit

18 years agoMinor changes.
Andrea Asperti [Mon, 5 Dec 2005 09:25:52 +0000 (09:25 +0000)]
Minor changes.

18 years agoremoved from repository spurious object files
Stefano Zacchiroli [Mon, 5 Dec 2005 09:22:45 +0000 (09:22 +0000)]
removed from repository spurious object files

18 years agoAdded a new section on the logical library.
Andrea Asperti [Mon, 5 Dec 2005 09:21:38 +0000 (09:21 +0000)]
Added a new section on the logical library.

18 years agometadata are no longer stored in .moo files.
Claudio Sacerdoti Coen [Sat, 3 Dec 2005 10:35:32 +0000 (10:35 +0000)]
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"

18 years ago1. metadata are no longer stored in .moo files.
Claudio Sacerdoti Coen [Sat, 3 Dec 2005 10:35:10 +0000 (10:35 +0000)]
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

18 years agomoved (and hence exported) uri rehashing functions on terms and objects to CicUtil
Stefano Zacchiroli [Fri, 2 Dec 2005 17:53:23 +0000 (17:53 +0000)]
moved (and hence exported) uri rehashing functions on terms and objects to CicUtil

18 years ago1. matitaEngine splitted into disambiguation (now in grafite_parser) and
Claudio Sacerdoti Coen [Fri, 2 Dec 2005 10:57:26 +0000 (10:57 +0000)]
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

18 years ago1. matitaEngine splitted into disambiguation (now in grafite_parser) and
Claudio Sacerdoti Coen [Fri, 2 Dec 2005 10:57:02 +0000 (10:57 +0000)]
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

18 years agoit may happen that matitaclean (clean_baseuris) calls the remove function
Enrico Tassi [Wed, 30 Nov 2005 16:26:21 +0000 (16:26 +0000)]
it may happen that matitaclean (clean_baseuris) calls the remove function
without having added the objects first... so the hashtbl is empty...
asert fasle -> []

18 years agomoved coercion to library (work in progress)
Claudio Sacerdoti Coen [Wed, 30 Nov 2005 14:43:50 +0000 (14:43 +0000)]
moved coercion to library (work in progress)

18 years agomoved coercions away (work in progress)
Claudio Sacerdoti Coen [Wed, 30 Nov 2005 14:43:32 +0000 (14:43 +0000)]
moved coercions away (work in progress)

18 years agocoercGraph.ml* moved from cic_unification to library
Claudio Sacerdoti Coen [Wed, 30 Nov 2005 12:33:06 +0000 (12:33 +0000)]
coercGraph.ml* moved from cic_unification to library

18 years agoImplicit aliases are now defined as all the aliases whose baseuri is the
Claudio Sacerdoti Coen [Wed, 30 Nov 2005 12:18:19 +0000 (12:18 +0000)]
Implicit aliases are now defined as all the aliases whose baseuri is the
baseuri of the current development. Much much cleaner.

18 years agonicer (but convertible) types
Claudio Sacerdoti Coen [Wed, 30 Nov 2005 12:17:53 +0000 (12:17 +0000)]
nicer (but convertible) types

18 years ago* Undo fixed.
Claudio Sacerdoti Coen [Wed, 30 Nov 2005 11:59:27 +0000 (11:59 +0000)]
* Undo fixed.
* Minor code cleaning.

18 years agoTerms parsed by notations were not localized.
Claudio Sacerdoti Coen [Wed, 30 Nov 2005 10:59:52 +0000 (10:59 +0000)]
Terms parsed by notations were not localized.

18 years agoimproved disambiguation section
Stefano Zacchiroli [Wed, 30 Nov 2005 10:48:35 +0000 (10:48 +0000)]
improved disambiguation section

18 years agoGeneration of auxiliary lemmas for inductive types and records moved
Claudio Sacerdoti Coen [Wed, 30 Nov 2005 10:11:00 +0000 (10:11 +0000)]
Generation of auxiliary lemmas for inductive types and records moved
from cic_proof_checking and matita to ocaml/library.

18 years ago* Part of matita that used to deal with the library moved into ocaml/library
Claudio Sacerdoti Coen [Tue, 29 Nov 2005 14:53:34 +0000 (14:53 +0000)]
* Part of matita that used to deal with the library moved into ocaml/library
* cic_unification/coercDb.ml* ==> library/coercDb.ml*

18 years agoAdded a few bibliographic entries.
Andrea Asperti [Tue, 29 Nov 2005 14:22:56 +0000 (14:22 +0000)]
Added a few bibliographic entries.

18 years agocoa continued
Ferruccio Guidi [Mon, 28 Nov 2005 19:42:52 +0000 (19:42 +0000)]
coa continued

18 years ago* More error messages localized.
Claudio Sacerdoti Coen [Mon, 28 Nov 2005 15:48:40 +0000 (15:48 +0000)]
* More error messages localized.
* Bug fixed: a few Uncertain became RefineFailure in my last commit(s).

18 years agoMore errors localized.
Claudio Sacerdoti Coen [Mon, 28 Nov 2005 15:26:50 +0000 (15:26 +0000)]
More errors localized.

18 years agoMore error messages localized.
Claudio Sacerdoti Coen [Mon, 28 Nov 2005 13:59:31 +0000 (13:59 +0000)]
More error messages localized.

18 years agoMore aggressive politic for non localized terms: an assert false!
Claudio Sacerdoti Coen [Mon, 28 Nov 2005 13:25:04 +0000 (13:25 +0000)]
More aggressive politic for non localized terms: an assert false!

18 years agofirst part on disambiguation passes
Stefano Zacchiroli [Mon, 28 Nov 2005 13:01:50 +0000 (13:01 +0000)]
first part on disambiguation passes

18 years agoadded comment
Enrico Tassi [Mon, 28 Nov 2005 12:59:23 +0000 (12:59 +0000)]
added comment

18 years agoDisambiguationError exceptions (that have locations inside) are now relocated
Claudio Sacerdoti Coen [Mon, 28 Nov 2005 12:58:02 +0000 (12:58 +0000)]
DisambiguationError exceptions (that have locations inside) are now relocated
correctly after a (** comment *).

18 years ago1. Bug fixed: compilation of "let corec" to a simple CoFix without a surrounding
Claudio Sacerdoti Coen [Mon, 28 Nov 2005 12:41:21 +0000 (12:41 +0000)]
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"

18 years agoremoved deadcode / fixed typos (thanks to ocaml 3.09)
Stefano Zacchiroli [Sun, 27 Nov 2005 16:17:59 +0000 (16:17 +0000)]
removed deadcode / fixed typos (thanks to ocaml 3.09)

18 years agoremoved dead code (thanks to ocaml 3.09)
Stefano Zacchiroli [Sun, 27 Nov 2005 16:17:36 +0000 (16:17 +0000)]
removed dead code (thanks to ocaml 3.09)

18 years agocrosso compatibility patch which enable building both with ocaml 3.08 and 3.09
Stefano Zacchiroli [Sun, 27 Nov 2005 15:53:47 +0000 (15:53 +0000)]
crosso compatibility patch which enable building both with ocaml 3.08 and 3.09

18 years agoocaml 3.09 transition
Stefano Zacchiroli [Sat, 26 Nov 2005 19:29:58 +0000 (19:29 +0000)]
ocaml 3.09 transition

18 years ago* wrong comments removed
Claudio Sacerdoti Coen [Sat, 26 Nov 2005 18:05:10 +0000 (18:05 +0000)]
* wrong comments removed
* relocalization of refined terms is now performed for every refined term

18 years agoRefinement bug fixed. The outtype was not refined if it was an Implicit.
Claudio Sacerdoti Coen [Sat, 26 Nov 2005 17:38:23 +0000 (17:38 +0000)]
Refinement bug fixed. The outtype was not refined if it was an Implicit.

18 years agocoimplication (continued)
Ferruccio Guidi [Sat, 26 Nov 2005 17:20:21 +0000 (17:20 +0000)]
coimplication (continued)
complete overlap algebras (started)

18 years agoDebugging code removed.
Claudio Sacerdoti Coen [Sat, 26 Nov 2005 16:41:01 +0000 (16:41 +0000)]
Debugging code removed.

18 years agoBug fixed: an unrefined term was passed around while checking explicit named
Claudio Sacerdoti Coen [Sat, 26 Nov 2005 16:23:34 +0000 (16:23 +0000)]
Bug fixed: an unrefined term was passed around while checking explicit named
substitutions.

18 years agoExperimental localization of errors during refinement and disambiguation.
Claudio Sacerdoti Coen [Sat, 26 Nov 2005 15:49:23 +0000 (15:49 +0000)]
Experimental localization of errors during refinement and disambiguation.

18 years agothe coimplication connective (start)
Ferruccio Guidi [Sat, 26 Nov 2005 15:39:02 +0000 (15:39 +0000)]
the coimplication connective (start)

18 years agoModule CicHash (hash-tables over CIC terms based on physical equality) moved
Claudio Sacerdoti Coen [Sat, 26 Nov 2005 11:56:07 +0000 (11:56 +0000)]
Module CicHash (hash-tables over CIC terms based on physical equality) moved
into Cic.

18 years agos/0c2/0c2a/ in .install
Stefano Zacchiroli [Sat, 26 Nov 2005 00:32:02 +0000 (00:32 +0000)]
s/0c2/0c2a/ in .install

18 years ago...
Claudio Sacerdoti Coen [Fri, 25 Nov 2005 18:07:41 +0000 (18:07 +0000)]
...

18 years agoNon exhaustive match fixed.
Claudio Sacerdoti Coen [Fri, 25 Nov 2005 17:40:38 +0000 (17:40 +0000)]
Non exhaustive match fixed.

18 years agoBug fixed: removal of .__log was not always attempted.
Stefano Zacchiroli [Fri, 25 Nov 2005 16:37:53 +0000 (16:37 +0000)]
Bug fixed: removal of .__log was not always attempted.

18 years agouse empty universe in the mono alias phases
Stefano Zacchiroli [Fri, 25 Nov 2005 16:34:17 +0000 (16:34 +0000)]
use empty universe in the mono alias phases

18 years agobugfix: removed unneeded No_choices exception
Stefano Zacchiroli [Fri, 25 Nov 2005 16:33:25 +0000 (16:33 +0000)]
bugfix: removed unneeded No_choices exception
bugfix: avoid looking in the library when explecitely asked not to do so

18 years agoConfronto con Coq.
Claudio Sacerdoti Coen [Fri, 25 Nov 2005 15:22:51 +0000 (15:22 +0000)]
Confronto con Coq.

18 years agominor changes
Stefano Zacchiroli [Fri, 25 Nov 2005 14:36:01 +0000 (14:36 +0000)]
minor changes

18 years agolabels
Stefano Zacchiroli [Fri, 25 Nov 2005 12:12:07 +0000 (12:12 +0000)]
labels

18 years ago...
Claudio Sacerdoti Coen [Fri, 25 Nov 2005 12:09:51 +0000 (12:09 +0000)]
...

18 years ago...
Claudio Sacerdoti Coen [Fri, 25 Nov 2005 12:09:18 +0000 (12:09 +0000)]
...

18 years agodeps
Stefano Zacchiroli [Fri, 25 Nov 2005 12:09:08 +0000 (12:09 +0000)]
deps

18 years agoMore on the presentation.
Claudio Sacerdoti Coen [Fri, 25 Nov 2005 11:59:33 +0000 (11:59 +0000)]
More on the presentation.

18 years agofix
Enrico Tassi [Fri, 25 Nov 2005 11:27:00 +0000 (11:27 +0000)]
fix

18 years agoadded missing deps
Stefano Zacchiroli [Fri, 25 Nov 2005 11:24:28 +0000 (11:24 +0000)]
added missing deps

18 years ago...
Claudio Sacerdoti Coen [Fri, 25 Nov 2005 11:19:59 +0000 (11:19 +0000)]
...

18 years agobuild paper per default
Stefano Zacchiroli [Fri, 25 Nov 2005 11:12:05 +0000 (11:12 +0000)]
build paper per default

18 years agodependency graphs
Stefano Zacchiroli [Fri, 25 Nov 2005 11:11:41 +0000 (11:11 +0000)]
dependency graphs

18 years agonotation intro
Stefano Zacchiroli [Fri, 25 Nov 2005 11:11:27 +0000 (11:11 +0000)]
notation intro

18 years agoadded tinycals and patterns subsections
Enrico Tassi [Fri, 25 Nov 2005 10:42:52 +0000 (10:42 +0000)]
added tinycals and patterns subsections

18 years agochanged META dependency
Stefano Zacchiroli [Fri, 25 Nov 2005 10:30:33 +0000 (10:30 +0000)]
changed META dependency
- disambiguation should (and actually does) depend only on acic_content
- paramodulation does not need disambiguation! (except for a test)

18 years agoUnused file removed.
Claudio Sacerdoti Coen [Fri, 25 Nov 2005 09:45:13 +0000 (09:45 +0000)]
Unused file removed.

18 years agoReshaped structure of ocaml/ libraries, matita changed accordingly.
Stefano Zacchiroli [Thu, 24 Nov 2005 18:26:49 +0000 (18:26 +0000)]
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

18 years agoReshaped structure of ocaml/ libraries.
Stefano Zacchiroli [Thu, 24 Nov 2005 18:25:43 +0000 (18:25 +0000)]
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

18 years ago...
Claudio Sacerdoti Coen [Thu, 24 Nov 2005 14:02:27 +0000 (14:02 +0000)]
...

18 years agoDa capo (matita2.tex).
Claudio Sacerdoti Coen [Thu, 24 Nov 2005 13:30:01 +0000 (13:30 +0000)]
Da capo (matita2.tex).

18 years agosplit non-logic level of whelp away from metadataQuery to a new module
Stefano Zacchiroli [Thu, 24 Nov 2005 13:01:31 +0000 (13:01 +0000)]
split non-logic level of whelp away from metadataQuery to a new module

18 years agoadded missing dependency
Stefano Zacchiroli [Thu, 24 Nov 2005 10:21:33 +0000 (10:21 +0000)]
added missing dependency

18 years agoremoved the need of REQUIRES in libraries Makefile, they are now queried from the...
Stefano Zacchiroli [Thu, 24 Nov 2005 08:39:51 +0000 (08:39 +0000)]
removed the need of REQUIRES in libraries Makefile, they are now queried from the corresponding META

18 years agobugfix: libraries.ps works again
Stefano Zacchiroli [Thu, 24 Nov 2005 08:38:53 +0000 (08:38 +0000)]
bugfix: libraries.ps works again

18 years agoprose
Stefano Zacchiroli [Thu, 24 Nov 2005 08:38:12 +0000 (08:38 +0000)]
prose

18 years agominimal introduction
Stefano Zacchiroli [Thu, 24 Nov 2005 08:38:03 +0000 (08:38 +0000)]
minimal introduction

18 years agoNew implementation for localized exceptions.
Claudio Sacerdoti Coen [Wed, 23 Nov 2005 22:31:36 +0000 (22:31 +0000)]
New implementation for localized exceptions.