]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agorebuit
Stefano Zacchiroli [Thu, 22 Apr 2004 13:53:22 +0000 (13:53 +0000)]
rebuit

20 years agoPatches to generate ?1 : ?2 : Type in place of ?1 : Type removed.
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 12:38:16 +0000 (12:38 +0000)]
Patches to generate ?1 : ?2 : Type in place of ?1 : Type removed.
It is interesting to understand whether it is still necessary (after
the CicUnification bug fix) or not.

20 years agoBig bug fixed: in the case t <?= ?1, the instantiation ?1 := t was generated
Enrico Tassi [Thu, 22 Apr 2004 12:33:35 +0000 (12:33 +0000)]
Big bug fixed: in the case  t <?= ?1, the instantiation ?1 := t was generated
and then t : C and ?1 : E were retrieved/computed correctly; then
E <?= T was incorrectly tested (instead of T <?= E).

20 years agofourier.mli addedto interface files.
Enrico Tassi [Thu, 22 Apr 2004 11:29:14 +0000 (11:29 +0000)]
fourier.mli addedto interface files.

20 years agosnapshot
Stefano Zacchiroli [Thu, 22 Apr 2004 10:41:14 +0000 (10:41 +0000)]
snapshot

20 years agoadded /help method (needed by respawner)
Stefano Zacchiroli [Thu, 22 Apr 2004 09:36:54 +0000 (09:36 +0000)]
added /help method (needed by respawner)

20 years agoIMPLEMENTATION_FILES now generated from INTERFACE_FILES.
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 09:11:16 +0000 (09:11 +0000)]
IMPLEMENTATION_FILES now generated from INTERFACE_FILES.

20 years agoadded .cvsignore
Stefano Zacchiroli [Thu, 22 Apr 2004 08:31:19 +0000 (08:31 +0000)]
added .cvsignore

20 years agodetects and uses {ocamlc,ocamlopt}.opt when available
Stefano Zacchiroli [Wed, 21 Apr 2004 17:46:17 +0000 (17:46 +0000)]
detects and uses {ocamlc,ocamlopt}.opt when available

20 years agodetect and use {ocamlc,ocamlopt}.opt when they are available
Stefano Zacchiroli [Wed, 21 Apr 2004 17:35:00 +0000 (17:35 +0000)]
detect and use {ocamlc,ocamlopt}.opt when they are available

20 years agoexported term_of_uri
Stefano Zacchiroli [Wed, 21 Apr 2004 17:29:35 +0000 (17:29 +0000)]
exported term_of_uri

20 years agoadded helmLibraryObjects.mli mention
Stefano Zacchiroli [Wed, 21 Apr 2004 17:26:39 +0000 (17:26 +0000)]
added helmLibraryObjects.mli mention

20 years agoadded .mli
Stefano Zacchiroli [Wed, 21 Apr 2004 16:36:38 +0000 (16:36 +0000)]
added .mli

20 years agogot rid of a ~status label
Stefano Zacchiroli [Tue, 20 Apr 2004 17:00:53 +0000 (17:00 +0000)]
got rid of a ~status label

20 years agogot rid of ~status label
Stefano Zacchiroli [Tue, 20 Apr 2004 17:00:27 +0000 (17:00 +0000)]
got rid of ~status label

20 years agogot rid of ~status label so that tactics can now be applied partially,
Stefano Zacchiroli [Tue, 20 Apr 2004 17:00:07 +0000 (17:00 +0000)]
got rid of ~status label so that tactics can now be applied partially,
delta reduced, ...

20 years agoadded ocamlfind library checks to configure.ac
Stefano Zacchiroli [Tue, 20 Apr 2004 09:41:10 +0000 (09:41 +0000)]
added ocamlfind library checks to configure.ac

20 years agorenamed mathita to matita
Stefano Zacchiroli [Tue, 20 Apr 2004 09:27:36 +0000 (09:27 +0000)]
renamed mathita to matita

20 years agosnapshot
Stefano Zacchiroli [Tue, 20 Apr 2004 08:54:23 +0000 (08:54 +0000)]
snapshot

20 years agoignore Makefile since now it's generated by configure
Stefano Zacchiroli [Mon, 19 Apr 2004 12:12:35 +0000 (12:12 +0000)]
ignore Makefile since now it's generated by configure

20 years agoadded Makefile.in
Stefano Zacchiroli [Mon, 19 Apr 2004 12:12:16 +0000 (12:12 +0000)]
added Makefile.in

20 years agoreorganized metas so that pxp is references only through helm-pxp
Stefano Zacchiroli [Mon, 19 Apr 2004 12:10:37 +0000 (12:10 +0000)]
reorganized metas so that pxp is references only through helm-pxp

20 years agoadded hbugs' (client) meta
Stefano Zacchiroli [Mon, 19 Apr 2004 12:10:20 +0000 (12:10 +0000)]
added hbugs' (client) meta

20 years agogeneralized META.* ignoring
Stefano Zacchiroli [Mon, 19 Apr 2004 12:10:03 +0000 (12:10 +0000)]
generalized META.* ignoring

20 years ago- reordered modules so that pxp could be used as entry point for pxp
Stefano Zacchiroli [Mon, 19 Apr 2004 12:09:22 +0000 (12:09 +0000)]
- reordered modules so that pxp could be used as entry point for pxp
- added hbugs
- pretty printed modules

20 years ago- use PxpHelmConf
Stefano Zacchiroli [Mon, 19 Apr 2004 12:08:35 +0000 (12:08 +0000)]
- use PxpHelmConf
- no longer use deprecated Pxp_yacc module

20 years ago- use PxpHelmConf
Stefano Zacchiroli [Mon, 19 Apr 2004 12:08:13 +0000 (12:08 +0000)]
- use PxpHelmConf
- no longer use deprecated Pxp_yacc

20 years agouse PxpHelmConf
Stefano Zacchiroli [Mon, 19 Apr 2004 12:07:51 +0000 (12:07 +0000)]
use PxpHelmConf

20 years agoadded dep on Helm_registry
Stefano Zacchiroli [Mon, 19 Apr 2004 12:07:37 +0000 (12:07 +0000)]
added dep on Helm_registry

20 years agouse PxpHelmConf module
Stefano Zacchiroli [Mon, 19 Apr 2004 12:07:12 +0000 (12:07 +0000)]
use PxpHelmConf module

20 years ago- use PxpHelmConf
Stefano Zacchiroli [Mon, 19 Apr 2004 12:06:56 +0000 (12:06 +0000)]
- use PxpHelmConf
- removed references to deprecated Pxp_yacc module

20 years ago- embedded ClientHTTP module (not very nice, but ClientHTTP shouldn't
Stefano Zacchiroli [Mon, 19 Apr 2004 12:06:25 +0000 (12:06 +0000)]
- embedded ClientHTTP module (not very nice, but ClientHTTP shouldn't
  belongs to Getter module!)
- added PxpHelmConf module, repository of Pxp configurations for helm

20 years agoadded ExtThread module, ex Hbugs_deity (a Thread module with killing
Stefano Zacchiroli [Mon, 19 Apr 2004 12:05:30 +0000 (12:05 +0000)]
added ExtThread module, ex Hbugs_deity (a Thread module with killing
capabilities)

20 years agoinjected hbugs under ocaml/ dir
Stefano Zacchiroli [Mon, 19 Apr 2004 12:04:26 +0000 (12:04 +0000)]
injected hbugs under ocaml/ dir

20 years agomoved hbugs under ocaml/
Stefano Zacchiroli [Mon, 19 Apr 2004 12:01:03 +0000 (12:01 +0000)]
moved hbugs under ocaml/

20 years agofixed a typo (inside a comment)
Stefano Zacchiroli [Mon, 19 Apr 2004 08:38:12 +0000 (08:38 +0000)]
fixed a typo (inside a comment)

20 years agotest_equality_only was not used in sort comparison.
Claudio Sacerdoti Coen [Fri, 16 Apr 2004 17:15:35 +0000 (17:15 +0000)]
test_equality_only was not used in sort comparison.
It should be implemented only in unification.

20 years agouse respawner
Stefano Zacchiroli [Fri, 16 Apr 2004 16:39:14 +0000 (16:39 +0000)]
use respawner

20 years agochanged logging message
Stefano Zacchiroli [Fri, 16 Apr 2004 16:39:01 +0000 (16:39 +0000)]
changed logging message

20 years agoremoved deprecated uwobo_forever.sh
Stefano Zacchiroli [Fri, 16 Apr 2004 16:16:36 +0000 (16:16 +0000)]
removed deprecated uwobo_forever.sh

20 years agoremoved tedious "_mowgli" postfix
Stefano Zacchiroli [Fri, 16 Apr 2004 16:16:01 +0000 (16:16 +0000)]
removed tedious "_mowgli" postfix

20 years agouse new daemon_respawner.sh
Stefano Zacchiroli [Fri, 16 Apr 2004 16:02:38 +0000 (16:02 +0000)]
use new daemon_respawner.sh

20 years agofixed some typos in sample init.d
Stefano Zacchiroli [Fri, 16 Apr 2004 16:02:27 +0000 (16:02 +0000)]
fixed some typos in sample init.d

20 years agoadded generic daemon respawner
Stefano Zacchiroli [Fri, 16 Apr 2004 15:56:20 +0000 (15:56 +0000)]
added generic daemon respawner

20 years agoscript deprecated
Stefano Zacchiroli [Fri, 16 Apr 2004 15:56:08 +0000 (15:56 +0000)]
script deprecated

20 years agoadded newline to log when log_file is in use
Stefano Zacchiroli [Fri, 16 Apr 2004 12:16:08 +0000 (12:16 +0000)]
added newline to log when log_file is in use

20 years ago- addead autoconf-iguration. Actually it only set the default runtime
Stefano Zacchiroli [Fri, 16 Apr 2004 08:43:20 +0000 (08:43 +0000)]
- addead autoconf-iguration. Actually it only set the default runtime
  configuration file

20 years ago- use new logger interface
Stefano Zacchiroli [Fri, 16 Apr 2004 08:18:39 +0000 (08:18 +0000)]
- use new logger interface
- added support for log_level and log_file in configuration file

20 years ago- rewritten http_getter logger interface
Stefano Zacchiroli [Fri, 16 Apr 2004 08:18:07 +0000 (08:18 +0000)]
- rewritten http_getter logger interface

20 years ago- added sample usage of get_opt method
Stefano Zacchiroli [Fri, 16 Apr 2004 08:17:38 +0000 (08:17 +0000)]
- added sample usage of get_opt method
- added method get_opt_default (like get_opt with an additional default
  value)

20 years agoMetasenv added as parameter to eta_fixing.
Andrea Asperti [Thu, 15 Apr 2004 16:47:42 +0000 (16:47 +0000)]
Metasenv added as parameter to eta_fixing.

20 years agos/dtd_base_url/dtd_base_urls/
Stefano Zacchiroli [Thu, 15 Apr 2004 13:36:31 +0000 (13:36 +0000)]
s/dtd_base_url/dtd_base_urls/

20 years ago- better pretty printing of exceptions (added red color)
Stefano Zacchiroli [Thu, 15 Apr 2004 13:35:53 +0000 (13:35 +0000)]
- better pretty printing of exceptions (added red color)
- added "-update" command line parameter for batch updating

20 years ago- fixed dtd_base_urls implementation
Stefano Zacchiroli [Thu, 15 Apr 2004 13:35:21 +0000 (13:35 +0000)]
- fixed dtd_base_urls implementation
- factorized a lot of code in document patching

20 years ago- better pretty printing on /update
Stefano Zacchiroli [Thu, 15 Apr 2004 13:35:00 +0000 (13:35 +0000)]
- better pretty printing on /update
- added stdout logger

20 years agoadded string_of_html_tag (plain text pretty printer for tags)
Stefano Zacchiroli [Thu, 15 Apr 2004 12:52:24 +0000 (12:52 +0000)]
added string_of_html_tag (plain text pretty printer for tags)

20 years agoadded support for multiple dtd_base_urls
Stefano Zacchiroli [Thu, 15 Apr 2004 12:25:40 +0000 (12:25 +0000)]
added support for multiple dtd_base_urls

20 years agoupdating all sections
Ferruccio Guidi [Wed, 14 Apr 2004 17:33:12 +0000 (17:33 +0000)]
updating all sections

20 years agopatched
Ferruccio Guidi [Wed, 14 Apr 2004 16:07:10 +0000 (16:07 +0000)]
patched

20 years agoBug fixed: the following happened.
Claudio Sacerdoti Coen [Wed, 14 Apr 2004 14:11:52 +0000 (14:11 +0000)]
Bug fixed: the following happened.
Auto generated two goals.
Closing the first goal instantiated also the second goal.
But we were still iterating over the original list of goals ==> BOOM!

20 years agoadded exists_meta
Stefano Zacchiroli [Wed, 14 Apr 2004 13:56:47 +0000 (13:56 +0000)]
added exists_meta

20 years agopatched
Ferruccio Guidi [Wed, 14 Apr 2004 11:25:09 +0000 (11:25 +0000)]
patched

20 years agoupdating the introduction
Ferruccio Guidi [Tue, 13 Apr 2004 15:58:12 +0000 (15:58 +0000)]
updating the introduction

20 years agoported to latest polymorphic variant types
Stefano Zacchiroli [Fri, 9 Apr 2004 15:09:28 +0000 (15:09 +0000)]
ported to latest polymorphic variant types

20 years agoAdded flag test_equality_only to are_convertible to better implement
Claudio Sacerdoti Coen [Wed, 7 Apr 2004 14:30:41 +0000 (14:30 +0000)]
Added flag test_equality_only to are_convertible to better implement
the <=_{\beta\delta\iota\zeta} relation.

20 years agoAdded flag test_equality_only to are_convertible (to better implement
Claudio Sacerdoti Coen [Wed, 7 Apr 2004 14:29:25 +0000 (14:29 +0000)]
Added flag test_equality_only to are_convertible (to better implement
the <=_{\beta\delta\iota\zeta} relation).

20 years agoadded a missing <br> tag
Stefano Zacchiroli [Wed, 7 Apr 2004 12:42:37 +0000 (12:42 +0000)]
added a missing <br> tag

20 years agoimplemented save_to
Stefano Zacchiroli [Tue, 6 Apr 2004 12:43:51 +0000 (12:43 +0000)]
implemented save_to

20 years ago- uncommented save_to function (now implemented)
Stefano Zacchiroli [Tue, 6 Apr 2004 12:43:43 +0000 (12:43 +0000)]
- uncommented save_to function (now implemented)
- added (tiny) description of the 'variable interpolation' feature

20 years agoadded Unix dependency (needed in order to run xmllint)
Stefano Zacchiroli [Tue, 6 Apr 2004 12:43:02 +0000 (12:43 +0000)]
added Unix dependency (needed in order to run xmllint)

20 years agoeta_fixing of the CurrentProof metasenv is wrong, since eta_fix does not have
Stefano Zacchiroli [Tue, 6 Apr 2004 12:38:20 +0000 (12:38 +0000)]
eta_fixing of the CurrentProof metasenv is wrong, since eta_fix does not have
the context parameter. Fixed by avoiding CurrentProof metasenv eta_fixing.

20 years agoThe parser accepts terms with metavariables as statements of theorems ==>
Stefano Zacchiroli [Tue, 6 Apr 2004 12:08:23 +0000 (12:08 +0000)]
The parser accepts terms with metavariables as statements of theorems ==>
metavariable instantiation must be propagated also on the theorem statement.

20 years ago- added test file
Stefano Zacchiroli [Tue, 6 Apr 2004 09:56:08 +0000 (09:56 +0000)]
- added test file

20 years ago- added via_http parameter so that when the getter is used locally (i.e.
Stefano Zacchiroli [Tue, 6 Apr 2004 09:53:26 +0000 (09:53 +0000)]
- added via_http parameter so that when the getter is used locally (i.e.
  as a library), http specific messages aren't generated
- use polymorphic variants for some configuration parameters
- better logging on /update (<br> tags are now generated)

20 years ago- use polymorphic variants for some configuration parameters
Stefano Zacchiroli [Tue, 6 Apr 2004 09:52:10 +0000 (09:52 +0000)]
- use polymorphic variants for some configuration parameters

20 years agobugfix: local context and canonical context previously don't have the
Stefano Zacchiroli [Tue, 6 Apr 2004 09:50:39 +0000 (09:50 +0000)]
bugfix: local context and canonical context previously don't have the
same length

20 years agobugfix: the function that abstract constant occurrences by putting metavariables
Stefano Zacchiroli [Tue, 6 Apr 2004 09:04:45 +0000 (09:04 +0000)]
bugfix: the function that abstract constant occurrences by putting metavariables
in place of identity explicit substitutions (local contexts) is generalized to
put ?1 : ?2 : Type in place of a ?1 : Type to take care of <Type in contravariant
position. Note: this is still partially bugged (see previous commit on the same
topic).

20 years agoreorganized functions order
Stefano Zacchiroli [Tue, 6 Apr 2004 09:02:18 +0000 (09:02 +0000)]
reorganized functions order

20 years agohttp_getter.conf.xml ==> /projects/helm/etc/http_getter.conf.xml
Claudio Sacerdoti Coen [Mon, 5 Apr 2004 17:32:45 +0000 (17:32 +0000)]
http_getter.conf.xml ==> /projects/helm/etc/http_getter.conf.xml

20 years agoadded html_of_html_tag
Stefano Zacchiroli [Mon, 5 Apr 2004 17:22:29 +0000 (17:22 +0000)]
added html_of_html_tag

20 years agoURL patching in ENTITY declarations extended to cover also absolute URLs.
Claudio Sacerdoti Coen [Mon, 5 Apr 2004 16:57:44 +0000 (16:57 +0000)]
URL patching in ENTITY declarations extended to cover also absolute URLs.

20 years agoXHTML character entities (used in the internal subset of .theory.xml files).
Claudio Sacerdoti Coen [Mon, 5 Apr 2004 16:49:13 +0000 (16:49 +0000)]
XHTML character entities (used in the internal subset of .theory.xml files).

20 years agoAdded a new function in_cache to cicEnvironemt. It takes an uri
Andrea Asperti [Mon, 5 Apr 2004 13:58:54 +0000 (13:58 +0000)]
Added a new function in_cache to cicEnvironemt. It takes an uri
and returns true or false according to the fact that uri is or
is not in the cache

20 years agoht:DEFINITION/Definition differentiated into
Claudio Sacerdoti Coen [Sun, 4 Apr 2004 13:44:08 +0000 (13:44 +0000)]
ht:DEFINITION/Definition differentiated into
 ht:DEFINITION/Definition and
 ht:DEFINITION/InteractiveDefinition

because of an explicit request of Iris Loeb.

20 years agos/per_user_settings/user_settings/ for consistency with gTopLevel
Stefano Zacchiroli [Fri, 2 Apr 2004 12:20:14 +0000 (12:20 +0000)]
s/per_user_settings/user_settings/ for consistency with gTopLevel
configuration file

20 years ago- logging of long-running actions (like update) is now sent to the
Stefano Zacchiroli [Fri, 2 Apr 2004 11:51:04 +0000 (11:51 +0000)]
- logging of long-running actions (like update) is now sent to the
  client incrementally
- moved some frontend related functions (like return_html*) from
  Http_getter_common to the frontend (main.ml)

20 years agoremoved no longer needed password from connection string
Stefano Zacchiroli [Thu, 1 Apr 2004 17:06:27 +0000 (17:06 +0000)]
removed no longer needed password from connection string

20 years ago- added "Host:" line to http requests so that virtual hosting hosts are
Stefano Zacchiroli [Thu, 1 Apr 2004 16:59:09 +0000 (16:59 +0000)]
- added "Host:" line to http requests so that virtual hosting hosts are
  supported (and ancient HTTP are no longer supported)

20 years ago- removed http_get/http_get_iter implementations, use the analogous
Stefano Zacchiroli [Thu, 1 Apr 2004 16:58:00 +0000 (16:58 +0000)]
- removed http_get/http_get_iter implementations, use the analogous
  functions from ocaml-http

20 years ago<VARIABLE as="LocalFact"/> added
Claudio Sacerdoti Coen [Thu, 1 Apr 2004 16:40:46 +0000 (16:40 +0000)]
<VARIABLE as="LocalFact"/> added

20 years agoremoved an out of date comment
Stefano Zacchiroli [Thu, 1 Apr 2004 15:45:08 +0000 (15:45 +0000)]
removed an out of date comment

20 years agoadded hyperlinks to help message
Stefano Zacchiroli [Thu, 1 Apr 2004 15:44:50 +0000 (15:44 +0000)]
added hyperlinks to help message

20 years agoremoved out of date configuration file
Stefano Zacchiroli [Thu, 1 Apr 2004 10:14:46 +0000 (10:14 +0000)]
removed out of date configuration file

20 years agotacticChaser modified to avoid double "apply" and to avoid to apply uris ".var" in...
Matteo Selmi [Wed, 31 Mar 2004 20:21:56 +0000 (20:21 +0000)]
tacticChaser modified to avoid double "apply" and to avoid to apply uris ".var" in tactic "auto".

20 years agoMeta files are in METAS subdir
Lionel Mamane [Wed, 31 Mar 2004 14:54:52 +0000 (14:54 +0000)]
Meta files are in METAS subdir
source of meta files are called meta., not META.

20 years agoInstall to findlib-defined dest dir, not to stdlib dir
Lionel Mamane [Wed, 31 Mar 2004 11:51:56 +0000 (11:51 +0000)]
Install to findlib-defined dest dir, not to stdlib dir

20 years ago- provastruct.theory.xml removed (what was that exactly?)
Claudio Sacerdoti Coen [Tue, 30 Mar 2004 16:36:09 +0000 (16:36 +0000)]
- provastruct.theory.xml removed (what was that exactly?)
- @name of SECTION renamed to @uri

20 years agoupdating and structuring
Ferruccio Guidi [Sun, 28 Mar 2004 11:06:45 +0000 (11:06 +0000)]
updating and structuring

20 years agoAlgebra => CoRN
Claudio Sacerdoti Coen [Fri, 26 Mar 2004 14:58:17 +0000 (14:58 +0000)]
Algebra => CoRN

20 years agotex notation enabled
Claudio Sacerdoti Coen [Fri, 26 Mar 2004 14:55:16 +0000 (14:55 +0000)]
tex notation enabled