]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years ago- removed unwind: every substitution is now _not_ unwinded
Stefano Zacchiroli [Mon, 2 Feb 2004 16:14:56 +0000 (16:14 +0000)]
- removed unwind: every substitution is now _not_ unwinded
- removed extra metasenv argument from all kernel proxies
- added kernel proxy: subst (for CicSubstitution.subst)
- added pretty printer ppterm

20 years agochanged prototype of CicMetaSubst.apply_subst*
Stefano Zacchiroli [Mon, 2 Feb 2004 16:11:37 +0000 (16:11 +0000)]
changed prototype of CicMetaSubst.apply_subst*

20 years agoadded comments
Stefano Zacchiroli [Mon, 2 Feb 2004 16:10:49 +0000 (16:10 +0000)]
added comments

20 years agofact regtest
Stefano Zacchiroli [Mon, 2 Feb 2004 14:53:48 +0000 (14:53 +0000)]
fact regtest

20 years agoreordered
Stefano Zacchiroli [Fri, 30 Jan 2004 08:15:01 +0000 (08:15 +0000)]
reordered

20 years agoadded string_of_html_msg
Stefano Zacchiroli [Fri, 30 Jan 2004 08:14:19 +0000 (08:14 +0000)]
added string_of_html_msg

20 years ago- typo bugfix: INT token no longer exists
Stefano Zacchiroli [Fri, 30 Jan 2004 08:13:56 +0000 (08:13 +0000)]
- typo bugfix: INT token no longer exists
- use "=" instead of \def for let definitions
- added a new "binder" level so that \forall n. n=n binds correctly

20 years agoRefinement of Fix and CoFix now implemented.
Claudio Sacerdoti Coen [Fri, 30 Jan 2004 08:13:29 +0000 (08:13 +0000)]
Refinement of Fix and CoFix now implemented.

20 years ago- removed ancient refine exception
Stefano Zacchiroli [Fri, 30 Jan 2004 08:11:56 +0000 (08:11 +0000)]
- removed ancient refine exception
- s/Try every selection/Try selected/ on a button

20 years agoadded regression tests
Stefano Zacchiroli [Fri, 30 Jan 2004 08:10:16 +0000 (08:10 +0000)]
added regression tests

20 years agos/Callbacks/DisambiguateCallbacks/
Stefano Zacchiroli [Fri, 30 Jan 2004 08:08:51 +0000 (08:08 +0000)]
s/Callbacks/DisambiguateCallbacks/

20 years ago- lift added to CicMetaSubst
Claudio Sacerdoti Coen [Thu, 29 Jan 2004 18:35:14 +0000 (18:35 +0000)]
- lift added to CicMetaSubst
- refine of Fix and CoFix implemented
- bug fixed in refine of Cast

20 years ago- s/TexTermEditor/TermEditor/ (* former no longer appropriate)
Stefano Zacchiroli [Thu, 29 Jan 2004 14:53:16 +0000 (14:53 +0000)]
- s/TexTermEditor/TermEditor/ (* former no longer appropriate)
- added "auto disambiguation" setting support

20 years ago- added "clear alias" menu item
Stefano Zacchiroli [Thu, 29 Jan 2004 13:25:52 +0000 (13:25 +0000)]
- added "clear alias" menu item
- added "clear" button to the "edit aliases" window

20 years ago- occur check test anticipated to the delift phase
Stefano Zacchiroli [Tue, 27 Jan 2004 17:30:09 +0000 (17:30 +0000)]
- occur check test anticipated to the delift phase
- uses CicUtil.lookup_meta

20 years agouse CicUtil.lookup_meta
Stefano Zacchiroli [Tue, 27 Jan 2004 17:29:18 +0000 (17:29 +0000)]
use CicUtil.lookup_meta

20 years agobad link patched
Ferruccio Guidi [Tue, 27 Jan 2004 17:25:43 +0000 (17:25 +0000)]
bad link patched

20 years agos/List.find.../CicUtil.lookup_meta/
Stefano Zacchiroli [Tue, 27 Jan 2004 17:08:31 +0000 (17:08 +0000)]
s/List.find.../CicUtil.lookup_meta/

20 years agoadded CicUtil module with just lookup_meta function
Stefano Zacchiroli [Tue, 27 Jan 2004 17:07:44 +0000 (17:07 +0000)]
added CicUtil module with just lookup_meta function

20 years agoempty goal patched
Ferruccio Guidi [Tue, 27 Jan 2004 13:47:37 +0000 (13:47 +0000)]
empty goal patched

20 years agoopt goal fixed
Ferruccio Guidi [Tue, 27 Jan 2004 13:36:06 +0000 (13:36 +0000)]
opt goal fixed

20 years agotest for empty string given, if so return Environment.empty without invoking the...
Andrea Asperti [Tue, 27 Jan 2004 12:32:25 +0000 (12:32 +0000)]
test for empty string given, if so return Environment.empty without invoking the parser

20 years agohelm registry's META
Stefano Zacchiroli [Tue, 27 Jan 2004 11:51:39 +0000 (11:51 +0000)]
helm registry's META

20 years agohelm registry --- first release
Stefano Zacchiroli [Tue, 27 Jan 2004 11:48:55 +0000 (11:48 +0000)]
helm registry --- first release

20 years agosample aliases language
Stefano Zacchiroli [Tue, 27 Jan 2004 08:47:53 +0000 (08:47 +0000)]
sample aliases language

20 years agoNotation for Case revisited and completed.
Andrea Asperti [Mon, 26 Jan 2004 13:40:46 +0000 (13:40 +0000)]
Notation for Case revisited and completed.

20 years agoGenerated ml files added.
Claudio Sacerdoti Coen [Mon, 26 Jan 2004 10:14:53 +0000 (10:14 +0000)]
Generated ml files added.

20 years agoraise proper exception when a regexp fails on term_of_uri
Stefano Zacchiroli [Mon, 26 Jan 2004 00:03:37 +0000 (00:03 +0000)]
raise proper exception when a regexp fails on term_of_uri

20 years agodon't remove METAs on clean, but on distclean
Stefano Zacchiroli [Sat, 24 Jan 2004 17:01:36 +0000 (17:01 +0000)]
don't remove METAs on clean, but on distclean

20 years ago- s/id_to_uris/environment/
Stefano Zacchiroli [Sat, 24 Jan 2004 17:00:58 +0000 (17:00 +0000)]
- s/id_to_uris/environment/
- bugfix: aliases work again

20 years agoreference moved EnvironmentP3 for new parser
Stefano Zacchiroli [Sat, 24 Jan 2004 17:00:18 +0000 (17:00 +0000)]
reference moved EnvironmentP3 for new parser

20 years ago- factorized DisambiguateChoices module
Stefano Zacchiroli [Sat, 24 Jan 2004 16:59:45 +0000 (16:59 +0000)]
- factorized DisambiguateChoices module
- implemented alias language for gTopLevel

20 years agooptionalizide some class parameters
Stefano Zacchiroli [Sat, 24 Jan 2004 16:58:48 +0000 (16:58 +0000)]
optionalizide some class parameters

20 years ago.in version of "configuration" modules
Stefano Zacchiroli [Sat, 24 Jan 2004 12:35:09 +0000 (12:35 +0000)]
.in version of "configuration" modules

20 years agodebug_print
Stefano Zacchiroli [Sat, 24 Jan 2004 12:34:41 +0000 (12:34 +0000)]
debug_print

20 years agonew configure.ac with support for compile time configuration of termeditor/parser/...
Stefano Zacchiroli [Sat, 24 Jan 2004 12:33:42 +0000 (12:33 +0000)]
new configure.ac with support for compile time configuration of termeditor/parser/...

20 years agosplit a term0 rule for dinamycally change top-level (i.e. non-recursive) term rul
Stefano Zacchiroli [Sat, 24 Jan 2004 12:32:04 +0000 (12:32 +0000)]
split a term0 rule for dinamycally change top-level (i.e. non-recursive) term rul

20 years agocollapsed parens in a singol token
Stefano Zacchiroli [Sat, 24 Jan 2004 12:31:30 +0000 (12:31 +0000)]
collapsed parens in a singol token

20 years agoadded tex notation
Stefano Zacchiroli [Sat, 24 Jan 2004 12:31:05 +0000 (12:31 +0000)]
added tex notation

20 years agotex notation for compatibility with texTermEditor
Stefano Zacchiroli [Sat, 24 Jan 2004 12:29:57 +0000 (12:29 +0000)]
tex notation for compatibility with texTermEditor

20 years ago- quiet debugging for mathql
Stefano Zacchiroli [Sat, 24 Jan 2004 12:29:26 +0000 (12:29 +0000)]
- quiet debugging for mathql
- defined a debug_print function with a verbosity level

20 years agoEureka!
Claudio Sacerdoti Coen [Fri, 23 Jan 2004 17:45:29 +0000 (17:45 +0000)]
Eureka!
It is now possible to choose independently:

 - the widget for the term editor
 - the disambiguating parser, i.e.
   * the parsing component
   * the disambiguating component

20 years agoported to new module names
Stefano Zacchiroli [Fri, 23 Jan 2004 17:41:28 +0000 (17:41 +0000)]
ported to new module names

20 years agohandle Cic.Anonymous
Stefano Zacchiroli [Fri, 23 Jan 2004 17:41:17 +0000 (17:41 +0000)]
handle Cic.Anonymous

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.