]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agoToolbox: preliminary version
Ferruccio Guidi [Fri, 6 May 2005 18:21:16 +0000 (18:21 +0000)]
Toolbox: preliminary version

19 years agoadded syntax for rewrite (TODO no rewrite-in-Hyp syntax)
Enrico Tassi [Fri, 6 May 2005 10:13:16 +0000 (10:13 +0000)]
added syntax for rewrite (TODO no rewrite-in-Hyp syntax)
bold sequent line
more space between the sequent line and the formulae

19 years agofactorization of rewrite.
Enrico Tassi [Fri, 6 May 2005 10:12:16 +0000 (10:12 +0000)]
factorization of rewrite.
now the tactic also does a beta reduction step
(behaving as expected)

19 years ago- ported to new CicParser interface which requires an uri argument to be
Stefano Zacchiroli [Thu, 5 May 2005 15:55:37 +0000 (15:55 +0000)]
- ported to new CicParser interface which requires an uri argument to be
  passed to parsing functions
- removed orrible hack for sort parsing

19 years agoadded "tags" target to generate vim tags with otags
Stefano Zacchiroli [Thu, 5 May 2005 15:54:53 +0000 (15:54 +0000)]
added "tags" target to generate vim tags with otags

19 years agoadded test and test.opt targets
Stefano Zacchiroli [Thu, 5 May 2005 15:54:34 +0000 (15:54 +0000)]
added test and test.opt targets

19 years ago- implemented CicPushParser which parser CIC objects using Expat
Stefano Zacchiroli [Thu, 5 May 2005 15:54:14 +0000 (15:54 +0000)]
- implemented CicPushParser which parser CIC objects using Expat
  (currently, old PXP parser have been renamed to CicPxpParser, new one
  has been named CicPushParser and CicParser can includes one of the
  two. It includes CicPushParser per default)
- added mandatory uri parameter to main parsing functions, it is needed
  for creation of universes when Type sorts are encountered

19 years ago- added .cvsignore
Stefano Zacchiroli [Thu, 5 May 2005 15:35:16 +0000 (15:35 +0000)]
- added .cvsignore
- removed test.ml (which has been promoted to extractor.ml)

19 years agotest_instance.ma
Andrea Asperti [Thu, 5 May 2005 14:15:51 +0000 (14:15 +0000)]
test_instance.ma

19 years agoSome modifications due to instance.
Andrea Asperti [Thu, 5 May 2005 11:14:14 +0000 (11:14 +0000)]
Some modifications due to instance.

19 years agoadded .depend
Stefano Zacchiroli [Thu, 5 May 2005 08:02:57 +0000 (08:02 +0000)]
added .depend

19 years agoadded extractor_manager
Enrico Tassi [Wed, 4 May 2005 13:25:58 +0000 (13:25 +0000)]
added extractor_manager

19 years agoadded new extractor based on MetadataDb.index_obj
Enrico Tassi [Tue, 3 May 2005 17:12:49 +0000 (17:12 +0000)]
added new extractor based on MetadataDb.index_obj

19 years agosync with SqlStatements
Enrico Tassi [Tue, 3 May 2005 14:43:12 +0000 (14:43 +0000)]
sync with SqlStatements

19 years agoadded DROP statements to sqlStatements
Enrico Tassi [Tue, 3 May 2005 14:37:30 +0000 (14:37 +0000)]
added DROP statements to sqlStatements

19 years agomore friendly sqlStatements api
Enrico Tassi [Tue, 3 May 2005 13:55:07 +0000 (13:55 +0000)]
more friendly sqlStatements api

19 years agoadded examples
Enrico Tassi [Tue, 3 May 2005 13:40:53 +0000 (13:40 +0000)]
added examples

19 years agoadded table_creator (comman line frontend to SqlStatements)
Enrico Tassi [Tue, 3 May 2005 13:39:34 +0000 (13:39 +0000)]
added table_creator (comman line frontend to SqlStatements)

19 years agoadded sqlStatements module (contains all CREATE TABLE/INDEX)
Enrico Tassi [Tue, 3 May 2005 13:38:25 +0000 (13:38 +0000)]
added sqlStatements module (contains all CREATE TABLE/INDEX)

19 years agoadded instance
Enrico Tassi [Tue, 3 May 2005 12:50:34 +0000 (12:50 +0000)]
added instance

19 years agofix for instance
Enrico Tassi [Tue, 3 May 2005 12:50:12 +0000 (12:50 +0000)]
fix for instance

19 years agoFirst version of instance.
Andrea Asperti [Tue, 3 May 2005 12:01:36 +0000 (12:01 +0000)]
First version of instance.

19 years agoattached auto
Enrico Tassi [Mon, 2 May 2005 13:58:45 +0000 (13:58 +0000)]
attached auto

19 years agoattached auto
Enrico Tassi [Mon, 2 May 2005 13:47:30 +0000 (13:47 +0000)]
attached auto

19 years agoadded the count table
Enrico Tassi [Mon, 2 May 2005 12:55:02 +0000 (12:55 +0000)]
added the count table

19 years agoadded Match (partially) and sync with the count table
Enrico Tassi [Mon, 2 May 2005 12:53:56 +0000 (12:53 +0000)]
added Match (partially) and sync with the count table

19 years agoadded ast for Match
Enrico Tassi [Mon, 2 May 2005 12:52:59 +0000 (12:52 +0000)]
added ast for Match

19 years agoremoved no_inconcl_aux, no_concl_hyp, no_hyp and added count
Enrico Tassi [Mon, 2 May 2005 12:52:30 +0000 (12:52 +0000)]
removed no_inconcl_aux, no_concl_hyp, no_hyp and added count

19 years agoadded more assertions on universes when loaded from dump (and fixed some bugs concern...
Enrico Tassi [Fri, 29 Apr 2005 18:52:57 +0000 (18:52 +0000)]
added more assertions on universes when loaded from dump (and fixed some bugs concerning re-hash-consing)

19 years agoadded the orrible hack to the parser that is needed to call CicUniv.fresh() properly
Enrico Tassi [Fri, 29 Apr 2005 18:52:08 +0000 (18:52 +0000)]
added the orrible hack to the parser that is needed to call CicUniv.fresh() properly

19 years agohint -> experimental_hint
Enrico Tassi [Fri, 29 Apr 2005 13:45:41 +0000 (13:45 +0000)]
hint -> experimental_hint

19 years agomain constants set is closed with constants types
Enrico Tassi [Fri, 29 Apr 2005 13:34:27 +0000 (13:34 +0000)]
main constants set is closed with constants types

19 years agoUniverseInconsistency is now wrapper by CicRefine.type_of_aux' to RefineFailure
Enrico Tassi [Fri, 29 Apr 2005 12:40:12 +0000 (12:40 +0000)]
UniverseInconsistency is now wrapper by CicRefine.type_of_aux' to RefineFailure

19 years agono more moogle... now whelp (config file name and daemon name)
Enrico Tassi [Fri, 29 Apr 2005 12:22:52 +0000 (12:22 +0000)]
no more moogle... now whelp (config file name and daemon name)

19 years agoadded dump/restore environment to the debug menu
Enrico Tassi [Fri, 29 Apr 2005 12:15:43 +0000 (12:15 +0000)]
added dump/restore environment to the debug menu
fixed bug: when proof is completed the browser@home is blank

19 years agoadded orrible hack to make the current uri visible in the parser so that named univer...
Enrico Tassi [Fri, 29 Apr 2005 12:13:58 +0000 (12:13 +0000)]
added orrible hack to make the current uri visible in the parser so that named universes are generated

19 years agocatched UniverseInconsistency
Enrico Tassi [Fri, 29 Apr 2005 12:13:05 +0000 (12:13 +0000)]
catched UniverseInconsistency
(only an hack, it should be wrapped by the refiner)

19 years agoadded parsing time benchmark
Enrico Tassi [Fri, 29 Apr 2005 12:12:08 +0000 (12:12 +0000)]
added parsing time benchmark
universes generation counter is now properly reset
added orrible hack to make the parser generate proper universes containig
  the uri

19 years agofixed a typo
Enrico Tassi [Fri, 29 Apr 2005 12:09:33 +0000 (12:09 +0000)]
fixed a typo

19 years agoadded parser benchamrk
Enrico Tassi [Fri, 29 Apr 2005 12:07:15 +0000 (12:07 +0000)]
added parser benchamrk

19 years agofix (ask Enrico :-)
Stefano Zacchiroli [Fri, 29 Apr 2005 08:08:49 +0000 (08:08 +0000)]
fix (ask Enrico :-)

19 years agouses CicUniv new assertions
Stefano Zacchiroli [Fri, 29 Apr 2005 08:07:53 +0000 (08:07 +0000)]
uses CicUniv new assertions

19 years agoadded assertions about graph in the environment having Some uris
Stefano Zacchiroli [Fri, 29 Apr 2005 08:07:05 +0000 (08:07 +0000)]
added assertions about graph in the environment having Some uris

19 years agoadded rating parameter to at_least (used by elim)
Stefano Zacchiroli [Fri, 29 Apr 2005 08:04:17 +0000 (08:04 +0000)]
added rating parameter to at_least (used by elim)

19 years agoattached macros: hint(partial), check
Enrico Tassi [Thu, 28 Apr 2005 14:12:22 +0000 (14:12 +0000)]
attached macros: hint(partial), check
now matitaScript has a mathviewer to show terms...

19 years agomoved "hint" from Command to Macro
Enrico Tassi [Thu, 28 Apr 2005 13:32:42 +0000 (13:32 +0000)]
moved "hint" from Command to Macro

19 years agodeactivated coercions
Enrico Tassi [Thu, 28 Apr 2005 13:31:37 +0000 (13:31 +0000)]
deactivated coercions

19 years agosingle INSERT on multiple tuples
Enrico Tassi [Thu, 28 Apr 2005 13:30:40 +0000 (13:30 +0000)]
single INSERT on multiple tuples
cosmetic changes
vars are now indexed

19 years agoadded hbugs and mathql
Enrico Tassi [Thu, 28 Apr 2005 13:29:30 +0000 (13:29 +0000)]
added hbugs and mathql

19 years agorenamed hbugs hint costructors to match latest API
Stefano Zacchiroli [Wed, 27 Apr 2005 20:15:35 +0000 (20:15 +0000)]
renamed hbugs hint costructors to match latest API

19 years agobugfix: patched .ml.in instaned of .ml :-(
Stefano Zacchiroli [Wed, 27 Apr 2005 17:25:58 +0000 (17:25 +0000)]
bugfix: patched .ml.in instaned of .ml :-(

19 years agochecked in new version of matita from svn
Stefano Zacchiroli [Wed, 27 Apr 2005 17:21:01 +0000 (17:21 +0000)]
checked in new version of matita from svn

19 years agoremoved all matita files
Stefano Zacchiroli [Wed, 27 Apr 2005 17:11:30 +0000 (17:11 +0000)]
removed all matita files

19 years agoremoved all old matita files (kept in attic)
Stefano Zacchiroli [Wed, 27 Apr 2005 17:10:57 +0000 (17:10 +0000)]
removed all old matita files (kept in attic)

19 years agoported to svn-cvs merge
Stefano Zacchiroli [Wed, 27 Apr 2005 17:02:06 +0000 (17:02 +0000)]
ported to svn-cvs merge

19 years agomerged changes from the svn fork by me and Enrico
Stefano Zacchiroli [Wed, 27 Apr 2005 17:01:49 +0000 (17:01 +0000)]
merged changes from the svn fork by me and Enrico

19 years agomake also in utilities on whatever target
Stefano Zacchiroli [Wed, 27 Apr 2005 13:54:37 +0000 (13:54 +0000)]
make also in utilities on whatever target

19 years agocvsignore
Stefano Zacchiroli [Wed, 27 Apr 2005 13:50:23 +0000 (13:50 +0000)]
cvsignore

19 years agoremoved ancient cic_textual_parser (last live version tagged "dead_dir_walking")
Stefano Zacchiroli [Wed, 27 Apr 2005 13:45:11 +0000 (13:45 +0000)]
removed ancient cic_textual_parser (last live version tagged "dead_dir_walking")

19 years agoadded re-hash-consing of URIs embedded in universes
Stefano Zacchiroli [Wed, 27 Apr 2005 13:43:15 +0000 (13:43 +0000)]
added re-hash-consing of URIs embedded in universes

19 years agogetter with in memory tree of URIs
Stefano Zacchiroli [Wed, 27 Apr 2005 13:42:31 +0000 (13:42 +0000)]
getter with in memory tree of URIs

19 years agobetter checks on elim input, two conditions are now required for an
Stefano Zacchiroli [Wed, 27 Apr 2005 12:32:02 +0000 (12:32 +0000)]
better checks on elim input, two conditions are now required for an
input to elim to be valid:
1) before the disambiguation an indentifier has been given by the user
2) after the disambiguation a MutInd Cic term has been created

19 years agoclean also hypno_tbl
Stefano Zacchiroli [Tue, 26 Apr 2005 17:21:24 +0000 (17:21 +0000)]
clean also hypno_tbl

19 years agoadded test.opt target
Stefano Zacchiroli [Tue, 26 Apr 2005 17:21:12 +0000 (17:21 +0000)]
added test.opt target

19 years ago- ported to current metadata API
Stefano Zacchiroli [Tue, 26 Apr 2005 17:21:01 +0000 (17:21 +0000)]
- ported to current metadata API
- changes so that it does not index a single URI given on cmdline, but
  rather all the URIs contained in a file

19 years agoadded sample entry for environment_dump configuration variable
Stefano Zacchiroli [Sun, 24 Apr 2005 13:44:40 +0000 (13:44 +0000)]
added sample entry for environment_dump configuration variable

19 years agoadded CicEnvironment preloading
Stefano Zacchiroli [Sun, 24 Apr 2005 13:43:31 +0000 (13:43 +0000)]
added CicEnvironment preloading

19 years agoadded licence header
Stefano Zacchiroli [Sat, 23 Apr 2005 13:00:14 +0000 (13:00 +0000)]
added licence header

19 years agoadded license statement
Stefano Zacchiroli [Sat, 23 Apr 2005 12:59:16 +0000 (12:59 +0000)]
added license statement

19 years agoadded license header
Stefano Zacchiroli [Sat, 23 Apr 2005 12:58:07 +0000 (12:58 +0000)]
added license header

19 years agomade context and metasenv parameters of trivial disambiguator optional
Stefano Zacchiroli [Fri, 22 Apr 2005 15:24:31 +0000 (15:24 +0000)]
made context and metasenv parameters of trivial disambiguator optional

19 years agoadded Trivial module with a disambiguate_term implementation which took
Stefano Zacchiroli [Fri, 22 Apr 2005 15:05:52 +0000 (15:05 +0000)]
added Trivial module with a disambiguate_term implementation which took
a string as input and return a Cic.term (if the input is not ambiguous)

19 years agoremoved debugging print
Stefano Zacchiroli [Fri, 22 Apr 2005 08:36:42 +0000 (08:36 +0000)]
removed debugging print

19 years agouses new at_least with criteria on constants number difference
Stefano Zacchiroli [Fri, 22 Apr 2005 08:35:21 +0000 (08:35 +0000)]
uses new at_least with criteria on constants number difference

19 years agoadded filtering criteria on differences between number of constants in
Stefano Zacchiroli [Fri, 22 Apr 2005 08:34:45 +0000 (08:34 +0000)]
added filtering criteria on differences between number of constants in
hypothesis and conclusion, should handle better queries on terms with
metavariables

19 years ago- added no_hyp table
Stefano Zacchiroli [Fri, 22 Apr 2005 08:30:30 +0000 (08:30 +0000)]
- added no_hyp table
- changed constants number integer type to small int
- added comments describing tables

19 years agosplit precedence level of binders: \lambda has higher precedence than others
Stefano Zacchiroli [Thu, 21 Apr 2005 12:54:31 +0000 (12:54 +0000)]
split precedence level of binders: \lambda has higher precedence than others
this is the resulting precedences scheme:
  lambda > apply > infix operators > binders

19 years agoremoved ancient indirections for gTopLevel
Stefano Zacchiroli [Thu, 21 Apr 2005 12:08:31 +0000 (12:08 +0000)]
removed ancient indirections for gTopLevel

19 years agono longer build neither mathql nor hbugs per default
Stefano Zacchiroli [Thu, 21 Apr 2005 12:08:04 +0000 (12:08 +0000)]
no longer build neither mathql nor hbugs per default

19 years agobumped copyright years
Stefano Zacchiroli [Thu, 21 Apr 2005 12:07:41 +0000 (12:07 +0000)]
bumped copyright years

19 years agoutilities for creating environment dumps
Stefano Zacchiroli [Thu, 21 Apr 2005 12:07:24 +0000 (12:07 +0000)]
utilities for creating environment dumps

19 years ago(hopefully) final decision on precedence levels:
Stefano Zacchiroli [Thu, 21 Apr 2005 12:04:32 +0000 (12:04 +0000)]
(hopefully) final decision on precedence levels:
  binder > apply > infix operators

19 years agobugfixes:
Stefano Zacchiroli [Wed, 20 Apr 2005 16:47:32 +0000 (16:47 +0000)]
bugfixes:
- reference position using MetadataTypes.*_pos so that changing the
  position prefix fixes all the references
- don't generated dummy predicates which always suceed like ("mainConcl" OR
  "inConcl") for at_most checking

19 years agochanged binding strength of some parsing entries:
Stefano Zacchiroli [Wed, 20 Apr 2005 16:12:01 +0000 (16:12 +0000)]
changed binding strength of some parsing entries:
( a > b means a binds more tightly than b)
- now: infix operators > binders > application
- previous: application > infix operators > binders

19 years agoremoved spurious debugging prints
Stefano Zacchiroli [Wed, 20 Apr 2005 08:54:29 +0000 (08:54 +0000)]
removed spurious debugging prints

19 years agohtml-escapes user given expression when filling hidden field "expression"
Stefano Zacchiroli [Wed, 20 Apr 2005 08:45:32 +0000 (08:45 +0000)]
html-escapes user given expression when filling hidden field "expression"
in this way xml/html forbidden characters like "<" are converted to "&lt;"
and doesn't crash uwobo

19 years agobugfix: opt target should build html pages too
Stefano Zacchiroli [Fri, 8 Apr 2005 16:28:18 +0000 (16:28 +0000)]
bugfix: opt target should build html pages too

19 years agoadded clickable fingers
Stefano Zacchiroli [Fri, 8 Apr 2005 15:52:16 +0000 (15:52 +0000)]
added clickable fingers

19 years agochanged logo: whelp!
Stefano Zacchiroli [Fri, 8 Apr 2005 11:47:01 +0000 (11:47 +0000)]
changed logo: whelp!

19 years agothe description file was patched
Ferruccio Guidi [Fri, 8 Apr 2005 07:51:56 +0000 (07:51 +0000)]
the description file was patched

19 years agoinitial version of the "lambda-delta" calculus including:
Ferruccio Guidi [Fri, 1 Apr 2005 11:06:01 +0000 (11:06 +0000)]
initial version of the "lambda-delta" calculus including:

- Confluence of reduction
- Generation lemma
- Thinning lemma
- Substitution lemma
- Type Correctness
- Type Uniqueness
- Subject Reduction

19 years agodebian version 0.0.5-6
Stefano Zacchiroli [Wed, 30 Mar 2005 07:23:33 +0000 (07:23 +0000)]
debian version 0.0.5-6

19 years agorebuilt against ocaml 3.08.3
Stefano Zacchiroli [Tue, 29 Mar 2005 09:41:42 +0000 (09:41 +0000)]
rebuilt against ocaml 3.08.3

19 years agodebian: rebuilt against ocaml 3.08.3
Stefano Zacchiroli [Fri, 25 Mar 2005 23:45:48 +0000 (23:45 +0000)]
debian: rebuilt against ocaml 3.08.3

19 years agoremove x_gdome_caml.c generated source on "clean"
Stefano Zacchiroli [Fri, 25 Mar 2005 23:45:33 +0000 (23:45 +0000)]
remove x_gdome_caml.c generated source on "clean"

19 years agodebian: rebuilt against ocaml 3.08.2
Stefano Zacchiroli [Fri, 25 Mar 2005 23:44:44 +0000 (23:44 +0000)]
debian: rebuilt against ocaml 3.08.2

19 years agoBug fixed in assumption_tac: a missing (lift n) when a declaration
Claudio Sacerdoti Coen [Tue, 22 Mar 2005 16:05:54 +0000 (16:05 +0000)]
Bug fixed in assumption_tac: a missing (lift n) when a declaration
x : A := t is found in the context.

19 years ago- bugfix: do not fail when query_kind is missing (e.g. on /getpage)
Stefano Zacchiroli [Wed, 16 Mar 2005 16:33:10 +0000 (16:33 +0000)]
- bugfix: do not fail when query_kind is missing (e.g. on /getpage)
- bugfix: security, no longer subject to directory traversal (!)

19 years agouser smaller font in result page
Stefano Zacchiroli [Wed, 16 Mar 2005 16:21:44 +0000 (16:21 +0000)]
user smaller font in result page

19 years ago- new pretty printing of interpretations
Stefano Zacchiroli [Wed, 16 Mar 2005 16:17:03 +0000 (16:17 +0000)]
- new pretty printing of interpretations
- bugfix: interpretations are now remembered between pages
- more coherent look and feel