]> matita.cs.unibo.it Git - helm.git/log
projects / helm.git / log
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
helm.git
18 years agoAdded a parameter (empty list) to load_notation.
commit | commitdiff | tree
Andrea Asperti [Mon, 9 Jan 2006 11:49:23 +0000 (11:49 +0000)]
Added a parameter (empty list) to load_notation.

18 years agoadded again the bin files
commit | commitdiff | tree
Enrico Tassi [Mon, 9 Jan 2006 11:05:06 +0000 (11:05 +0000)]
added again the bin files

18 years agomoved away broken files
commit | commitdiff | tree
Enrico Tassi [Mon, 9 Jan 2006 11:04:12 +0000 (11:04 +0000)]
moved away broken files

18 years agoNew version of compare_weights.
commit | commitdiff | tree
Andrea Asperti [Mon, 9 Jan 2006 10:56:02 +0000 (10:56 +0000)]
New version of compare_weights.

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Mon, 9 Jan 2006 10:54:49 +0000 (10:54 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Mon, 9 Jan 2006 10:41:17 +0000 (10:41 +0000)]
fix

18 years agomoved to svn
commit | commitdiff | tree
Enrico Tassi [Mon, 9 Jan 2006 10:39:26 +0000 (10:39 +0000)]
moved to svn

18 years agoStupid bug of mine fixed: sometimes (Some ~-1) was used in place of None.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Mon, 9 Jan 2006 09:39:14 +0000 (09:39 +0000)]
Stupid bug of mine fixed: sometimes (Some ~-1) was used in place of None.
Moreover the userGoal was retrieved before setting it.

18 years agoNew version.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Mon, 9 Jan 2006 08:50:55 +0000 (08:50 +0000)]
New version.

18 years agoBug fixed: the include_paths were no longer handled properly when matita was
commit | commitdiff | tree
Claudio Sacerdoti Coen [Sun, 8 Jan 2006 19:16:27 +0000 (19:16 +0000)]
Bug fixed: the include_paths were no longer handled properly when matita was
launched outside a development. E.g.: ./matita library/nat/times.ma was no
longer working (./matita -I library library/nat/times.ma was)

18 years agoBug fixed: macros in the middle of a goto cursor or goto end-of-script were
commit | commitdiff | tree
Claudio Sacerdoti Coen [Sun, 8 Jan 2006 18:45:58 +0000 (18:45 +0000)]
Bug fixed: macros in the middle of a goto cursor or goto end-of-script were
not executed.

Explanation: the current goal was set only externally, but it is used by
macro disambiguation.

To fix the bug I have finally changed the type of a "lazy_macro" so that its
input is now a context. it used to be an integer, the selected goal; however,
the integer does not make sense since a macro can be invoked also when there is
no current proof.

18 years agoAdded $Id$ to every .ml file.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Sun, 8 Jan 2006 18:00:22 +0000 (18:00 +0000)]
Added $Id$ to every .ml file.

18 years agoAdded $Id$ to the file.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Sun, 8 Jan 2006 17:38:35 +0000 (17:38 +0000)]
Added $Id$ to the file.

18 years ago.cvsignore files removed (the svn:property property is used instead)
commit | commitdiff | tree
Claudio Sacerdoti Coen [Sun, 8 Jan 2006 17:26:52 +0000 (17:26 +0000)]
.cvsignore files removed (the svn:property property is used instead)

18 years ago1. Macros are now handled using an execption that is caught by matitacLib
commit | commitdiff | tree
Claudio Sacerdoti Coen [Sun, 8 Jan 2006 17:20:59 +0000 (17:20 +0000)]
1. Macros are now handled using an execption that is caught by matitacLib
   (raising an error) or matitaScript. As a result matitaScript is now simpler.
2. svn:ignore property refined for several directories in ocaml

18 years agoported to ocaml 3.09.1
commit | commitdiff | tree
Stefano Zacchiroli [Sun, 8 Jan 2006 12:14:20 +0000 (12:14 +0000)]
ported to ocaml 3.09.1

18 years agoported to ocaml 3.09.1
commit | commitdiff | tree
Stefano Zacchiroli [Sun, 8 Jan 2006 00:31:58 +0000 (00:31 +0000)]
ported to ocaml 3.09.1

18 years agobugfix, removed an hard coded instances of ocaml ABI version
commit | commitdiff | tree
Stefano Zacchiroli [Sun, 8 Jan 2006 00:28:27 +0000 (00:28 +0000)]
bugfix, removed an hard coded instances of ocaml ABI version

18 years agoported to ocaml 3.09.1
commit | commitdiff | tree
Stefano Zacchiroli [Sun, 8 Jan 2006 00:22:53 +0000 (00:22 +0000)]
ported to ocaml 3.09.1

18 years agoported to ocaml 3.09.1
commit | commitdiff | tree
Stefano Zacchiroli [Sat, 7 Jan 2006 17:54:03 +0000 (17:54 +0000)]
ported to ocaml 3.09.1

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Mon, 26 Dec 2005 11:41:21 +0000 (11:41 +0000)]
fix

18 years agobeauty\!
commit | commitdiff | tree
Enrico Tassi [Sat, 24 Dec 2005 14:44:04 +0000 (14:44 +0000)]
beauty\!

18 years agobeauty\!
commit | commitdiff | tree
Enrico Tassi [Sat, 24 Dec 2005 14:40:26 +0000 (14:40 +0000)]
beauty\!

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Sat, 24 Dec 2005 14:10:47 +0000 (14:10 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Sat, 24 Dec 2005 14:01:00 +0000 (14:01 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Sat, 24 Dec 2005 13:57:47 +0000 (13:57 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Sat, 24 Dec 2005 13:54:59 +0000 (13:54 +0000)]
fix

18 years agomore fix
commit | commitdiff | tree
Enrico Tassi [Sat, 24 Dec 2005 13:44:54 +0000 (13:44 +0000)]
more fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Sat, 24 Dec 2005 13:36:51 +0000 (13:36 +0000)]
fix

18 years agoattempt to move nightly profiling to svn
commit | commitdiff | tree
Enrico Tassi [Sat, 24 Dec 2005 13:36:29 +0000 (13:36 +0000)]
attempt to move nightly profiling to svn

18 years agoremoved spurious CVSROOT from the old repository
commit | commitdiff | tree
Stefano Zacchiroli [Sat, 24 Dec 2005 12:09:12 +0000 (12:09 +0000)]
removed spurious CVSROOT from the old repository

18 years agotest commit
commit | commitdiff | tree
Enrico Tassi [Sat, 24 Dec 2005 11:32:17 +0000 (11:32 +0000)]
test commit

18 years agoremoved prova
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 23 Dec 2005 12:38:52 +0000 (12:38 +0000)]
removed prova

18 years agoprova
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 23 Dec 2005 12:38:21 +0000 (12:38 +0000)]
prova

18 years agoupdated
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 23 Dec 2005 10:48:20 +0000 (10:48 +0000)]
updated

18 years agominor fixes (-nodb works again)
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 23 Dec 2005 10:43:14 +0000 (10:43 +0000)]
minor fixes (-nodb works again)

18 years agoAdded parameter first_statement_only to the functions in matitaEngine
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 22 Dec 2005 18:05:32 +0000 (18:05 +0000)]
Added parameter first_statement_only to the functions in matitaEngine

18 years agoalias diffing/insertion is now handled by matitaEngine (invoked both
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 22 Dec 2005 16:18:06 +0000 (16:18 +0000)]
alias diffing/insertion is now handled by matitaEngine (invoked both
by matita and matitac)

18 years agoMakefiles made less verbose.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 22 Dec 2005 13:32:45 +0000 (13:32 +0000)]
Makefiles made less verbose.

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Thu, 22 Dec 2005 10:26:21 +0000 (10:26 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Thu, 22 Dec 2005 10:18:31 +0000 (10:18 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Thu, 22 Dec 2005 10:02:40 +0000 (10:02 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Thu, 22 Dec 2005 10:01:37 +0000 (10:01 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Thu, 22 Dec 2005 09:59:19 +0000 (09:59 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Thu, 22 Dec 2005 09:56:14 +0000 (09:56 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Thu, 22 Dec 2005 09:47:52 +0000 (09:47 +0000)]
fix

18 years ago...
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 21 Dec 2005 18:18:09 +0000 (18:18 +0000)]
...

18 years agofixed -f in clean
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 16:24:20 +0000 (16:24 +0000)]
fixed -f in clean
make tests now compiles coq.ma

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 16:15:14 +0000 (16:15 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 16:15:14 +0000 (16:15 +0000)]
fix

18 years agoreimplemented specific marshallars on top of generic HMarshal marshaller
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 21 Dec 2005 16:12:01 +0000 (16:12 +0000)]
reimplemented specific marshallars on top of generic HMarshal marshaller

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 16:10:30 +0000 (16:10 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 16:03:08 +0000 (16:03 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 16:01:41 +0000 (16:01 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 16:00:38 +0000 (16:00 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 16:00:10 +0000 (16:00 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:59:34 +0000 (15:59 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:55:14 +0000 (15:55 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:54:14 +0000 (15:54 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:53:46 +0000 (15:53 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:49:59 +0000 (15:49 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:45:59 +0000 (15:45 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:45:21 +0000 (15:45 +0000)]
fix

18 years agoadded generic marshaller
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 21 Dec 2005 15:45:17 +0000 (15:45 +0000)]
added generic marshaller

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:44:23 +0000 (15:44 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:43:44 +0000 (15:43 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:41:36 +0000 (15:41 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:40:35 +0000 (15:40 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:39:27 +0000 (15:39 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:35:35 +0000 (15:35 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:34:23 +0000 (15:34 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:34:07 +0000 (15:34 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:32:44 +0000 (15:32 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:30:04 +0000 (15:30 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:29:05 +0000 (15:29 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:28:47 +0000 (15:28 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:27:05 +0000 (15:27 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:26:08 +0000 (15:26 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:25:25 +0000 (15:25 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:22:48 +0000 (15:22 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:19:50 +0000 (15:19 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:19:28 +0000 (15:19 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 15:01:08 +0000 (15:01 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 14:53:23 +0000 (14:53 +0000)]
fix

18 years agoold files
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 21 Dec 2005 14:36:59 +0000 (14:36 +0000)]
old files

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 14:35:54 +0000 (14:35 +0000)]
fix

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 14:35:21 +0000 (14:35 +0000)]
fix

18 years agoremoved old Makefile
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 21 Dec 2005 14:35:14 +0000 (14:35 +0000)]
removed old Makefile

18 years agofix
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 14:33:49 +0000 (14:33 +0000)]
fix

18 years agobench
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 14:32:37 +0000 (14:32 +0000)]
bench

18 years ago__ files are removed
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 14:22:22 +0000 (14:22 +0000)]
__ files are removed

18 years agono more "completed in ."
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 14:02:20 +0000 (14:02 +0000)]
no more "completed in ."

18 years agoHuge reorganization of matita and ocaml.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 21 Dec 2005 13:49:21 +0000 (13:49 +0000)]
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

18 years agoHuge reorganization of matita and ocaml.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 21 Dec 2005 13:49:17 +0000 (13:49 +0000)]
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

18 years agofixed cicbrowser.opt argv.(0)
commit | commitdiff | tree
Enrico Tassi [Wed, 21 Dec 2005 10:18:09 +0000 (10:18 +0000)]
fixed cicbrowser.opt argv.(0)

18 years agobugfix: typo which implied using the wrong pattern
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 20 Dec 2005 13:10:03 +0000 (13:10 +0000)]
bugfix: typo which implied using the wrong pattern

18 years agoadded ocamldep.opt checking
commit | commitdiff | tree
Enrico Tassi [Tue, 20 Dec 2005 09:28:05 +0000 (09:28 +0000)]
added ocamldep.opt checking

18 years agomoved term indexing (in both discrimination and path tree forms) from paramodulation...
commit | commitdiff | tree
Andrea Asperti [Mon, 19 Dec 2005 16:03:29 +0000 (16:03 +0000)]
moved term indexing (in both discrimination and path tree forms) from paramodulation/ to cic/

18 years agoDiscrimination and trie removed.
commit | commitdiff | tree
Andrea Asperti [Mon, 19 Dec 2005 13:57:45 +0000 (13:57 +0000)]
Discrimination and trie removed.

18 years agoupgraded dependency figures
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 19 Dec 2005 12:49:24 +0000 (12:49 +0000)]
upgraded dependency figures

next
Unnamed repository; edit this file 'description' to name the repository.