]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agosnapshot (notably: first working version of the console)
Stefano Zacchiroli [Tue, 4 May 2004 10:47:10 +0000 (10:47 +0000)]
snapshot (notably: first working version of the console)

20 years ago- moved up in the grammar precedences command entry so that sequence of
Stefano Zacchiroli [Tue, 4 May 2004 10:46:39 +0000 (10:46 +0000)]
- moved up in the grammar precedences command entry so that sequence of
  commands are not permitted
- added parsing of "abort" command

20 years agoremoved traliling dot in command pretty printer, now it's added by the
Stefano Zacchiroli [Tue, 4 May 2004 10:45:54 +0000 (10:45 +0000)]
removed traliling dot in command pretty printer, now it's added by the
tactical pp

20 years agoadded Abort and Check commands
Stefano Zacchiroli [Fri, 30 Apr 2004 14:00:15 +0000 (14:00 +0000)]
added Abort and Check commands

20 years agoembedded commands ast into tacticals ast
Stefano Zacchiroli [Fri, 30 Apr 2004 09:25:36 +0000 (09:25 +0000)]
embedded commands ast into tacticals ast

20 years ago- moved command as sub-entries of tactical grammars (as per tactics)
Stefano Zacchiroli [Fri, 30 Apr 2004 09:24:49 +0000 (09:24 +0000)]
- moved command as sub-entries of tactical grammars (as per tactics)

20 years agosnapshot
Stefano Zacchiroli [Fri, 30 Apr 2004 08:23:12 +0000 (08:23 +0000)]
snapshot

20 years ago- moved applyTransformation initialization code to the relevant library
Stefano Zacchiroli [Thu, 29 Apr 2004 16:15:25 +0000 (16:15 +0000)]
- moved applyTransformation initialization code to the relevant library
- decoupled termViewer from ChosenTransformer

20 years agomoved here initialization code (previously in gTopLevel/termViewer.ml)
Stefano Zacchiroli [Thu, 29 Apr 2004 16:14:33 +0000 (16:14 +0000)]
moved here initialization code (previously in gTopLevel/termViewer.ml)

20 years agosnapshot
Stefano Zacchiroli [Thu, 29 Apr 2004 13:59:11 +0000 (13:59 +0000)]
snapshot

20 years ago- added a configuration variable for selecting between fresh instances
Stefano Zacchiroli [Thu, 29 Apr 2004 13:55:31 +0000 (13:55 +0000)]
- added a configuration variable for selecting between fresh instances
  for numbers or not (set by default to a single instance)

20 years agosnapshot
Stefano Zacchiroli [Wed, 28 Apr 2004 20:45:38 +0000 (20:45 +0000)]
snapshot

20 years agoadded a TODO comment
Stefano Zacchiroli [Wed, 28 Apr 2004 20:45:16 +0000 (20:45 +0000)]
added a TODO comment

20 years agorebuilt
Stefano Zacchiroli [Wed, 28 Apr 2004 15:04:31 +0000 (15:04 +0000)]
rebuilt

20 years agoadded extra "id" parameter for input_or_locate_uri callback
Stefano Zacchiroli [Wed, 28 Apr 2004 15:04:11 +0000 (15:04 +0000)]
added extra "id" parameter for input_or_locate_uri callback

20 years ago- split logic operators away from aritmetic ones so that
Stefano Zacchiroli [Wed, 28 Apr 2004 14:11:51 +0000 (14:11 +0000)]
- split logic operators away from aritmetic ones so that
   \forall n:nat. n > 0 \or n = 0
  is parsed "correctly"

20 years agoremoved file:// prefix from local_library key, hopefully it isn't useful
Stefano Zacchiroli [Wed, 28 Apr 2004 14:00:42 +0000 (14:00 +0000)]
removed file:// prefix from local_library key, hopefully it isn't useful

20 years agosnapshot
Stefano Zacchiroli [Fri, 23 Apr 2004 14:54:46 +0000 (14:54 +0000)]
snapshot

20 years agogt URL pointed to lt
Claudio Sacerdoti Coen [Fri, 23 Apr 2004 12:57:29 +0000 (12:57 +0000)]
gt URL pointed to lt

20 years agoUniverses introduction
Enrico Tassi [Fri, 23 Apr 2004 10:37:00 +0000 (10:37 +0000)]
Universes introduction

20 years agordfly hardcoded URL changed from mowgli.cs.unibo.it to localhost
Claudio Sacerdoti Coen [Fri, 23 Apr 2004 10:03:12 +0000 (10:03 +0000)]
rdfly hardcoded URL changed from mowgli.cs.unibo.it to localhost

20 years agoexpandasking parameter passed to UWOBO.
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 17:00:31 +0000 (17:00 +0000)]
expandasking parameter passed to UWOBO.

20 years agosnapshot
Stefano Zacchiroli [Thu, 22 Apr 2004 16:33:02 +0000 (16:33 +0000)]
snapshot

20 years agomysql_connection.* keys added
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 15:02:50 +0000 (15:02 +0000)]
mysql_connection.* keys added

20 years agomathql_interpreter.mysql_connection.* keys added.
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 15:00:11 +0000 (15:00 +0000)]
mathql_interpreter.mysql_connection.* keys added.

20 years agoadded (and used) some type shorthands
Stefano Zacchiroli [Thu, 22 Apr 2004 13:54:12 +0000 (13:54 +0000)]
added (and used) some type shorthands

20 years ago- added some type shorthands
Stefano Zacchiroli [Thu, 22 Apr 2004 13:53:49 +0000 (13:53 +0000)]
- added some type shorthands
- added license information

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