]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agorenamed modules so that they are more consistent with other cic modules
Stefano Zacchiroli [Fri, 23 Jan 2004 17:05:20 +0000 (17:05 +0000)]
renamed modules so that they are more consistent with other cic modules

20 years agomoved environmentP3 in cic_textual_parser2 and reshaped interface
Stefano Zacchiroli [Fri, 23 Jan 2004 16:39:35 +0000 (16:39 +0000)]
moved environmentP3 in cic_textual_parser2 and reshaped interface

20 years agoimplemented interface for gTopLevel
Stefano Zacchiroli [Fri, 23 Jan 2004 16:38:17 +0000 (16:38 +0000)]
implemented interface for gTopLevel

20 years agomoved term_of_uri in cic/
Stefano Zacchiroli [Fri, 23 Jan 2004 16:37:57 +0000 (16:37 +0000)]
moved term_of_uri in cic/

20 years agomoved here term_of_uri
Stefano Zacchiroli [Fri, 23 Jan 2004 16:37:30 +0000 (16:37 +0000)]
moved here term_of_uri

20 years agobetter comment for kernel wrappers
Stefano Zacchiroli [Fri, 23 Jan 2004 16:37:14 +0000 (16:37 +0000)]
better comment for kernel wrappers

20 years agoa better error message
Stefano Zacchiroli [Fri, 23 Jan 2004 16:37:00 +0000 (16:37 +0000)]
a better error message

20 years ago- Added DisambiguatingParser (that abstracts both the parser and the
Claudio Sacerdoti Coen [Fri, 23 Jan 2004 15:30:33 +0000 (15:30 +0000)]
- Added DisambiguatingParser (that abstracts both the parser and the
  disambiguator used)
- Added ChosenTermEditor (used to swap quickly the editor used).
- moved disambiguate.ml* to oldDisambiguate.ml*

20 years ago...
Claudio Sacerdoti Coen [Fri, 23 Jan 2004 13:54:58 +0000 (13:54 +0000)]
...

20 years agoremoved useless -thread switch
Stefano Zacchiroli [Fri, 23 Jan 2004 13:47:49 +0000 (13:47 +0000)]
removed useless -thread switch

20 years agoported to latest lablgtk2 snapshot
Stefano Zacchiroli [Fri, 23 Jan 2004 12:52:59 +0000 (12:52 +0000)]
ported to latest lablgtk2 snapshot

20 years agoadded false test
Stefano Zacchiroli [Thu, 22 Jan 2004 17:19:17 +0000 (17:19 +0000)]
added false test

20 years ago- added -thread switch
Stefano Zacchiroli [Thu, 22 Jan 2004 16:45:58 +0000 (16:45 +0000)]
- added -thread switch
- reordered modules

20 years agobuild also cic_textual_parser2
Stefano Zacchiroli [Thu, 22 Jan 2004 16:38:54 +0000 (16:38 +0000)]
build also cic_textual_parser2

20 years agoupdated
Stefano Zacchiroli [Thu, 22 Jan 2004 16:37:16 +0000 (16:37 +0000)]
updated

20 years agoadded dependency to lablgtk2.glade
Stefano Zacchiroli [Thu, 22 Jan 2004 16:34:30 +0000 (16:34 +0000)]
added dependency to lablgtk2.glade

20 years agoadded -thread switch and dependency on lablgtk2.glade
Stefano Zacchiroli [Thu, 22 Jan 2004 16:24:49 +0000 (16:24 +0000)]
added -thread switch and dependency on lablgtk2.glade

20 years agomoved disambiguate module away
Stefano Zacchiroli [Thu, 22 Jan 2004 16:19:22 +0000 (16:19 +0000)]
moved disambiguate module away

20 years ago(temporary, waiting for abstraction over disambiguators) ported to Andrea &
Stefano Zacchiroli [Thu, 22 Jan 2004 16:07:42 +0000 (16:07 +0000)]
(temporary, waiting for abstraction over disambiguators) ported to Andrea &
Zack's disambiguator

20 years agoadded ChosenTransformer
Stefano Zacchiroli [Thu, 22 Jan 2004 15:54:59 +0000 (15:54 +0000)]
added ChosenTransformer

20 years agoabstracted over which transformer gTopLevel uses (ocaml or xslt)
Stefano Zacchiroli [Thu, 22 Jan 2004 15:50:16 +0000 (15:50 +0000)]
abstracted over which transformer gTopLevel uses (ocaml or xslt)

20 years agoNow applying ocaml transformations to sequents as well.
Andrea Asperti [Thu, 22 Jan 2004 15:45:42 +0000 (15:45 +0000)]
Now applying ocaml transformations to sequents as well.

20 years agoA few modifications, here and there...
Andrea Asperti [Thu, 22 Jan 2004 15:27:59 +0000 (15:27 +0000)]
A few modifications, here and there...

20 years agoAdded all transformations for sequents.
Andrea Asperti [Thu, 22 Jan 2004 15:23:01 +0000 (15:23 +0000)]
Added all transformations for sequents.

20 years agoThe parser have been made more functional with a trick.
Claudio Sacerdoti Coen [Thu, 22 Jan 2004 15:12:11 +0000 (15:12 +0000)]
The parser have been made more functional with a trick.
Now there is no more need to save and restore the metasenv.

20 years agouse "assert false" where needed
Stefano Zacchiroli [Thu, 22 Jan 2004 12:29:48 +0000 (12:29 +0000)]
use "assert false" where needed

20 years agoadded some match examples/regtests
Stefano Zacchiroli [Thu, 22 Jan 2004 12:27:02 +0000 (12:27 +0000)]
added some match examples/regtests

20 years agolocated parse error message
Stefano Zacchiroli [Thu, 22 Jan 2004 12:26:43 +0000 (12:26 +0000)]
located parse error message

20 years ago- bugfix: raise an Invalid_choice insteda of a generic exception on
Stefano Zacchiroli [Thu, 22 Jan 2004 12:25:36 +0000 (12:25 +0000)]
- bugfix: raise an Invalid_choice insteda of a generic exception on
  inductive constructor error
- moved TEST_INTERPRETATION debug message in a better place

20 years agoadded to CicMetaSubst subst wrapper for CicReduction.are_convertible
Stefano Zacchiroli [Thu, 22 Jan 2004 12:22:34 +0000 (12:22 +0000)]
added to CicMetaSubst subst wrapper for CicReduction.are_convertible

20 years ago- added backup target
Stefano Zacchiroli [Thu, 22 Jan 2004 12:22:02 +0000 (12:22 +0000)]
- added backup target
- use pattern rules instead of anciente prefix rules

20 years ago- removed some unneeded dependencies from debian/control
Stefano Zacchiroli [Thu, 22 Jan 2004 11:59:18 +0000 (11:59 +0000)]
- removed some unneeded dependencies from debian/control
- bumped standards-version

20 years agoTypo fixed.
Claudio Sacerdoti Coen [Thu, 22 Jan 2004 11:19:26 +0000 (11:19 +0000)]
Typo fixed.

20 years agoprettified
Stefano Zacchiroli [Thu, 22 Jan 2004 10:44:37 +0000 (10:44 +0000)]
prettified

20 years agouse new proofEngineHelpers
Stefano Zacchiroli [Thu, 22 Jan 2004 10:41:40 +0000 (10:41 +0000)]
use new proofEngineHelpers

20 years agomoved hard coded uris to HelmLibraryObjects
Stefano Zacchiroli [Thu, 22 Jan 2004 10:33:10 +0000 (10:33 +0000)]
moved hard coded uris to HelmLibraryObjects

20 years agoported to cicMetaSubst
Stefano Zacchiroli [Thu, 22 Jan 2004 10:32:52 +0000 (10:32 +0000)]
ported to cicMetaSubst

20 years ago- splitted into cicMetaSubst
Stefano Zacchiroli [Thu, 22 Jan 2004 10:31:33 +0000 (10:31 +0000)]
- splitted into cicMetaSubst
- bugfixes
- better exceptions

20 years agobugfixes, typos and the hell
Stefano Zacchiroli [Thu, 22 Jan 2004 10:30:52 +0000 (10:30 +0000)]
bugfixes, typos and the hell

20 years agosplit into this and cicMetaSubst.mli
Stefano Zacchiroli [Thu, 22 Jan 2004 10:29:33 +0000 (10:29 +0000)]
split into this and cicMetaSubst.mli

20 years agoadded CicMetaSubst module for metavariable instantiatiation
Stefano Zacchiroli [Thu, 22 Jan 2004 10:28:34 +0000 (10:28 +0000)]
added CicMetaSubst module for metavariable instantiatiation

20 years agobetter exception and error messages
Stefano Zacchiroli [Thu, 22 Jan 2004 10:26:32 +0000 (10:26 +0000)]
better exception and error messages

20 years ago- bugfix: print metas local context in the rigth order
Stefano Zacchiroli [Thu, 22 Jan 2004 10:24:50 +0000 (10:24 +0000)]
- bugfix: print metas local context in the rigth order
- renamed string_of_name to ppname and exported it

20 years agoFirst version of refine for MutCase, still largely incomplete.
Andrea Asperti [Tue, 20 Jan 2004 10:25:10 +0000 (10:25 +0000)]
First version of refine for MutCase, still largely incomplete.

20 years ago/projects/helm/log moved to /var/log/mowgli
Claudio Sacerdoti Coen [Tue, 20 Jan 2004 08:40:09 +0000 (08:40 +0000)]
/projects/helm/log moved to /var/log/mowgli

20 years ago/projects/helm/run/*_mowgli.pid moved into /var/run
Claudio Sacerdoti Coen [Tue, 20 Jan 2004 08:38:35 +0000 (08:38 +0000)]
/projects/helm/run/*_mowgli.pid moved into /var/run

20 years agoScripts simplified (since now we have only one cluster and only one
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 17:41:47 +0000 (17:41 +0000)]
Scripts simplified (since now we have only one cluster and only one
stable version of the library).

20 years agoNuPRL stuff moved.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 17:41:25 +0000 (17:41 +0000)]
NuPRL stuff moved.

20 years agoNo longer in use. The official repository for the
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 15:25:01 +0000 (15:25 +0000)]
No longer in use. The official repository for the
stylesheet is now the repository of mowgli.

20 years agoBranch V7_3_new_exportation merged.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 15:13:45 +0000 (15:13 +0000)]
Branch V7_3_new_exportation merged.

20 years agoError message updated.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 14:32:08 +0000 (14:32 +0000)]
Error message updated.

20 years agoNo more in use.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 14:31:29 +0000 (14:31 +0000)]
No more in use.

20 years agoTypo fixed.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 14:26:46 +0000 (14:26 +0000)]
Typo fixed.

20 years agoWe are now using the standard dot distribution of debian.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 14:26:22 +0000 (14:26 +0000)]
We are now using the standard dot distribution of debian.

20 years agoOnly V7_mowgli left.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 13:43:48 +0000 (13:43 +0000)]
Only V7_mowgli left.

20 years agoDaemons moved to /projects/helm/daemons.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:57:29 +0000 (12:57 +0000)]
Daemons moved to /projects/helm/daemons.

20 years agoDaemon moved to /projects/helm/daemons.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:41:15 +0000 (12:41 +0000)]
Daemon moved to /projects/helm/daemons.

20 years ago*** empty log message ***
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:36:02 +0000 (12:36 +0000)]
*** empty log message ***

20 years agoSeveral daemons moved into /projects/helm/daemons.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:35:23 +0000 (12:35 +0000)]
Several daemons moved into /projects/helm/daemons.

20 years agoErrore message improved.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:10:48 +0000 (12:10 +0000)]
Errore message improved.

20 years agoMissing package dependency.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:02:42 +0000 (12:02 +0000)]
Missing package dependency.

20 years agosnapshot, almost working
Stefano Zacchiroli [Mon, 19 Jan 2004 11:43:03 +0000 (11:43 +0000)]
snapshot, almost working
TODO:
- domain processing order
- notation generation

20 years agoadded a CSC's TODO comment
Stefano Zacchiroli [Mon, 19 Jan 2004 11:41:56 +0000 (11:41 +0000)]
added a CSC's TODO comment

20 years agoadded MkImplicit module for meta handling
Stefano Zacchiroli [Mon, 19 Jan 2004 11:39:59 +0000 (11:39 +0000)]
added MkImplicit module for meta handling

20 years agoadded Peano module and functions to create natural/real terms
Stefano Zacchiroli [Mon, 19 Jan 2004 11:38:41 +0000 (11:38 +0000)]
added Peano module and functions to create natural/real terms

20 years agoBranch V7_3_new_exportation closed.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 11:28:09 +0000 (11:28 +0000)]
Branch V7_3_new_exportation closed.

20 years agomathql listed twice
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 10:39:17 +0000 (10:39 +0000)]
mathql listed twice

20 years agoThe searchengine now requires the mathql_db_map.txt.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 10:12:48 +0000 (10:12 +0000)]
The searchengine now requires the mathql_db_map.txt.
Added the mathql_db_map.txt file and the new environment variable
MATHQL_DB_MAP.

20 years agoNo longer in use.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 09:54:59 +0000 (09:54 +0000)]
No longer in use.

20 years agoError in the warning message.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 09:52:20 +0000 (09:52 +0000)]
Error in the warning message.

20 years agoadded missing depending on (CSC's) helm-cic_textual_parser
Stefano Zacchiroli [Wed, 14 Jan 2004 18:07:41 +0000 (18:07 +0000)]
added missing depending on (CSC's) helm-cic_textual_parser

20 years agoremoved ui_logger, now in external module logger
Stefano Zacchiroli [Wed, 14 Jan 2004 18:04:41 +0000 (18:04 +0000)]
removed ui_logger, now in external module logger

20 years agoadded missing dependencies on mathql-*
Stefano Zacchiroli [Wed, 14 Jan 2004 18:03:26 +0000 (18:03 +0000)]
added missing dependencies on mathql-*

20 years agoadded logger's META
Stefano Zacchiroli [Wed, 14 Jan 2004 18:01:32 +0000 (18:01 +0000)]
added logger's META

20 years agomoved to the logger module
Stefano Zacchiroli [Wed, 14 Jan 2004 17:59:01 +0000 (17:59 +0000)]
moved to the logger module

20 years ago- added logger module
Stefano Zacchiroli [Wed, 14 Jan 2004 17:57:59 +0000 (17:57 +0000)]
- added logger module
- vertical ordering

20 years agomoved here ui_logger from gTopLeve
Stefano Zacchiroli [Wed, 14 Jan 2004 17:57:11 +0000 (17:57 +0000)]
moved here ui_logger from gTopLeve

20 years agostill a working copy, now towards a cleaner implementation ...
Stefano Zacchiroli [Wed, 14 Jan 2004 17:54:33 +0000 (17:54 +0000)]
still a working copy, now towards a cleaner implementation ...

20 years agoadded HelmLibraryObjects module
Stefano Zacchiroli [Mon, 12 Jan 2004 17:12:39 +0000 (17:12 +0000)]
added HelmLibraryObjects module

20 years ago* removed email address
Luca Padovani [Fri, 19 Dec 2003 09:34:20 +0000 (09:34 +0000)]
* removed email address

20 years agoBug commented out. The comment is also commented.
Claudio Sacerdoti Coen [Thu, 18 Dec 2003 14:42:06 +0000 (14:42 +0000)]
Bug commented out. The comment is also commented.

20 years agoBig bug spotted: restriction can fail and it was implicitly assumed that it
Claudio Sacerdoti Coen [Thu, 18 Dec 2003 13:17:51 +0000 (13:17 +0000)]
Big bug spotted: restriction can fail and it was implicitly assumed that it
didn't. Added another comment in the code.

20 years agoOne of the bug I detected (and commented) in my last commit was not a bug.
Claudio Sacerdoti Coen [Thu, 18 Dec 2003 10:46:18 +0000 (10:46 +0000)]
One of the bug I detected (and commented) in my last commit was not a bug.
This commit removes the erroneus comment.

20 years agopatched
Ferruccio Guidi [Wed, 17 Dec 2003 18:36:03 +0000 (18:36 +0000)]
patched

20 years agoMore comments. Some of them may highlight bugs or open issues.
Claudio Sacerdoti Coen [Wed, 17 Dec 2003 17:37:03 +0000 (17:37 +0000)]
More comments. Some of them may highlight bugs or open issues.

20 years agogenerate gui to temp file in order to catch lablgladecc2 failures
Stefano Zacchiroli [Wed, 17 Dec 2003 14:49:52 +0000 (14:49 +0000)]
generate gui to temp file in order to catch lablgladecc2 failures

20 years agorebuilt
Stefano Zacchiroli [Wed, 17 Dec 2003 14:41:28 +0000 (14:41 +0000)]
rebuilt

20 years agos/Logger/CicLogger/
Stefano Zacchiroli [Wed, 17 Dec 2003 14:11:32 +0000 (14:11 +0000)]
s/Logger/CicLogger/

20 years agouse ocaml-http instead of netclient for http requests
Stefano Zacchiroli [Wed, 17 Dec 2003 14:04:28 +0000 (14:04 +0000)]
use ocaml-http instead of netclient for http requests

20 years agoMakefiles patched
Ferruccio Guidi [Wed, 17 Dec 2003 11:52:28 +0000 (11:52 +0000)]
Makefiles patched

20 years agoBig bug spotted and commented: the delift function considers the explicit
Claudio Sacerdoti Coen [Wed, 17 Dec 2003 11:49:58 +0000 (11:49 +0000)]
Big bug spotted and commented: the delift function considers the explicit
substitution over metavariable occurrences as telescopic. Instead it is
simultaneous.

20 years ago* comments improved an possible code weakness (i.e. less than first order
Claudio Sacerdoti Coen [Wed, 17 Dec 2003 11:27:30 +0000 (11:27 +0000)]
* comments improved an possible code weakness (i.e. less than first order
  unification detected) made explicit in the comment and with a warning.

20 years ago* Reindentation
Claudio Sacerdoti Coen [Wed, 17 Dec 2003 10:47:40 +0000 (10:47 +0000)]
* Reindentation
* More comments

20 years ago* Reindentation.
Claudio Sacerdoti Coen [Wed, 17 Dec 2003 10:46:18 +0000 (10:46 +0000)]
* Reindentation.
* Useless code elimination.
* Debug code elimination.

20 years ago- ported to new output_html Disambiguate callback
Stefano Zacchiroli [Tue, 16 Dec 2003 17:56:42 +0000 (17:56 +0000)]
- ported to new output_html Disambiguate callback
- removed netclient dependency

20 years agos/netclient/http/ in dependencies
Stefano Zacchiroli [Tue, 16 Dec 2003 17:56:03 +0000 (17:56 +0000)]
s/netclient/http/ in dependencies

20 years agocosmetic changes
Stefano Zacchiroli [Tue, 16 Dec 2003 17:55:44 +0000 (17:55 +0000)]
cosmetic changes

20 years agouse ocaml-http instead of netclient for http GET requests
Stefano Zacchiroli [Tue, 16 Dec 2003 17:37:58 +0000 (17:37 +0000)]
use ocaml-http instead of netclient for http GET requests

20 years ago- use ocaml-http instead of netclient for http GET requests
Stefano Zacchiroli [Tue, 16 Dec 2003 17:34:08 +0000 (17:34 +0000)]
- use ocaml-http instead of netclient for http GET requests
- renamed Makefile targets so that all and clean have the usual
  semantics

20 years agoremoved old perl versions of graph daemons
Stefano Zacchiroli [Tue, 16 Dec 2003 17:33:25 +0000 (17:33 +0000)]
removed old perl versions of graph daemons