]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agoadded tinycals to the proof we frequently use for examples and screenshots
Stefano Zacchiroli [Wed, 26 Jul 2006 09:24:55 +0000 (09:24 +0000)]
added tinycals to the proof we frequently use for examples and screenshots

18 years agoadded test for reordering of goals when using the 1,2,3: tinycal
Stefano Zacchiroli [Wed, 26 Jul 2006 09:17:25 +0000 (09:17 +0000)]
added test for reordering of goals when using the 1,2,3: tinycal

18 years agoorder is important
Enrico Tassi [Wed, 26 Jul 2006 08:35:34 +0000 (08:35 +0000)]
order is important

18 years agoadded definition of f_equal1. I think this file should not be inside the matita library!
Enrico Tassi [Tue, 25 Jul 2006 09:04:25 +0000 (09:04 +0000)]
added definition of f_equal1. I think this file should not be inside the matita library!
once cercions from /\ to eq will be committed the definition should be replaced by two
coercion statement (that will generate the composite)

18 years agoBug fixed: a symbol alias Symb(s,0) now subsumes the case Symb(s,n) for each n.
Andrea Asperti [Mon, 24 Jul 2006 16:36:26 +0000 (16:36 +0000)]
Bug fixed: a symbol alias Symb(s,0) now subsumes the case Symb(s,n) for each n.

18 years agoDisambiguation passes simplified.
Claudio Sacerdoti Coen [Mon, 24 Jul 2006 14:58:55 +0000 (14:58 +0000)]
Disambiguation passes simplified.

18 years agoA compiling version of the library.
Andrea Asperti [Mon, 24 Jul 2006 14:50:33 +0000 (14:50 +0000)]
A compiling version of the library.

18 years agouse the new graphviz pretty printer API
Stefano Zacchiroli [Mon, 24 Jul 2006 14:28:13 +0000 (14:28 +0000)]
use the new graphviz pretty printer API

18 years agoadded missing dependency
Stefano Zacchiroli [Mon, 24 Jul 2006 14:09:40 +0000 (14:09 +0000)]
added missing dependency

18 years agoequality now requires 2 extra parameters
Stefano Zacchiroli [Mon, 24 Jul 2006 14:09:30 +0000 (14:09 +0000)]
equality now requires 2 extra parameters

18 years agoremoved reference to primes1.ma (now removed)
Stefano Zacchiroli [Mon, 24 Jul 2006 14:09:09 +0000 (14:09 +0000)]
removed reference to primes1.ma (now removed)

18 years agoadded timeout parameter to auto paramodulation.
Enrico Tassi [Mon, 24 Jul 2006 10:32:14 +0000 (10:32 +0000)]
added timeout parameter to auto paramodulation.

18 years agomore work on matitaprover (no more XML and buris are created).
Enrico Tassi [Mon, 24 Jul 2006 09:32:54 +0000 (09:32 +0000)]
more work on matitaprover (no more XML and buris are created).
now matita can start on a .p file.

18 years agomore and more tests
Enrico Tassi [Mon, 24 Jul 2006 08:07:07 +0000 (08:07 +0000)]
more and more tests

18 years agomore static libs for matitaprover
Enrico Tassi [Sun, 23 Jul 2006 09:06:33 +0000 (09:06 +0000)]
more static libs for matitaprover

18 years agosee BOO025-1 as an example of failure if (mot p) is commented out.
Enrico Tassi [Sun, 23 Jul 2006 08:36:35 +0000 (08:36 +0000)]
see BOO025-1 as an example of failure if (mot p) is commented out.

18 years agoadded
Enrico Tassi [Sat, 22 Jul 2006 17:17:47 +0000 (17:17 +0000)]
added

18 years agomatitaprover
Enrico Tassi [Sat, 22 Jul 2006 17:14:13 +0000 (17:14 +0000)]
matitaprover

18 years agoeta_fix default to false
Enrico Tassi [Fri, 21 Jul 2006 14:17:20 +0000 (14:17 +0000)]
eta_fix default to false

18 years agoRevert of the previous situation: when an identifier has no universe all the
Claudio Sacerdoti Coen [Thu, 20 Jul 2006 15:17:46 +0000 (15:17 +0000)]
Revert of the previous situation: when an identifier has no universe all the
passes that does not use the library are doomed to fail and the user will
be asked how to instantiate everyn identifier (not withstanding performances).
Now if an identifier has no universe we look for its interpretations in the
library.

18 years agotrans chains even inside letins body
Enrico Tassi [Thu, 20 Jul 2006 15:10:24 +0000 (15:10 +0000)]
trans chains even inside letins body

18 years agoavoid collapsing node that does not need to be, i.e.:
Stefano Zacchiroli [Thu, 20 Jul 2006 15:02:52 +0000 (15:02 +0000)]
avoid collapsing node that does not need to be, i.e.:
- nodes with no outgoing edges
- nodes which have not been expanded before

18 years agoremoved abstractios for dummy metavariables when generating letins body
Enrico Tassi [Thu, 20 Jul 2006 13:11:23 +0000 (13:11 +0000)]
removed abstractios for dummy metavariables when generating letins body

18 years agoreorganization
Enrico Tassi [Thu, 20 Jul 2006 11:22:15 +0000 (11:22 +0000)]
reorganization

18 years agobugfix: proper computation of the amount of new node shown upon expand
Stefano Zacchiroli [Thu, 20 Jul 2006 10:46:57 +0000 (10:46 +0000)]
bugfix: proper computation of the amount of new node shown upon expand

18 years agoadded -dot to generate dot files
Enrico Tassi [Thu, 20 Jul 2006 09:30:22 +0000 (09:30 +0000)]
added -dot to generate dot files

18 years ago- added to the cicBrowser support for displaying recursive direct/inverse
Stefano Zacchiroli [Wed, 19 Jul 2006 17:34:50 +0000 (17:34 +0000)]
- added to the cicBrowser support for displaying recursive direct/inverse
  dependencies of a given object. To integrate this with cicBrowser's history
  also added a new URI scheme: metadata:/deps/(forward|backward)/URI, where URI
  is the object URI without the trailing "cic:"
- removed automatic stripping of #xpointer(...) from URIs of inductive types

18 years agoNew module to extract from the Db direct and inverse dependencies starting from
Stefano Zacchiroli [Wed, 19 Jul 2006 17:32:43 +0000 (17:32 +0000)]
New module to extract from the Db direct and inverse dependencies starting from
a given URI. Both single step and recursive (in graph form) dependencies are
supported.

18 years agoexported position_prefix (so that it can be looked up from elsewhere)
Stefano Zacchiroli [Wed, 19 Jul 2006 17:31:20 +0000 (17:31 +0000)]
exported position_prefix (so that it can be looked up from elsewhere)

18 years agouse double quotes around escaped URIs, single quotes fail when the URI contains
Stefano Zacchiroli [Wed, 19 Jul 2006 17:30:32 +0000 (17:30 +0000)]
use double quotes around escaped URIs, single quotes fail when the URI contains
a '\'' character

18 years ago- enable header to output graphs attributes and graph-wide node and edge
Stefano Zacchiroli [Wed, 19 Jul 2006 17:29:44 +0000 (17:29 +0000)]
- enable header to output graphs attributes and graph-wide node and edge
  attributes
- quote nodes only when needed

18 years ago- pipe graphviz markup to tred before generating png/map output to get rid of
Stefano Zacchiroli [Wed, 19 Jul 2006 17:28:20 +0000 (17:28 +0000)]
- pipe graphviz markup to tred before generating png/map output to get rid of
  transitive dependencies
- added method center_on_href to clamp viewport so that a given node is visible
  (actually it is not a real "center"ing ...)

18 years agoBug fixed in rewrite in multiple hypothesis and/or conclusion: a lifting was
Claudio Sacerdoti Coen [Wed, 19 Jul 2006 16:29:06 +0000 (16:29 +0000)]
Bug fixed in rewrite in multiple hypothesis and/or conclusion: a lifting was
missing, as usual :-)

18 years ago- added sql statements for querying forward and backward dependencies
Stefano Zacchiroli [Wed, 19 Jul 2006 15:28:24 +0000 (15:28 +0000)]
- added sql statements for querying forward and backward dependencies
- escaped uri which get embedded in sql statements

18 years agoSubmitted a test for inferencing of dependent types.
Claudio Sacerdoti Coen [Wed, 19 Jul 2006 15:11:14 +0000 (15:11 +0000)]
Submitted a test for inferencing of dependent types.

18 years agoadded sets of uri pairs (useful for edges between uris)
Stefano Zacchiroli [Wed, 19 Jul 2006 10:43:43 +0000 (10:43 +0000)]
added sets of uri pairs (useful for edges between uris)
currently commented since not used ...

18 years agoCtr-C now cleans up (with a nice warning :-)
Claudio Sacerdoti Coen [Wed, 19 Jul 2006 10:04:02 +0000 (10:04 +0000)]
Ctr-C now cleans up (with a nice warning :-)

18 years agois_empty_listing fixed: the ls method normalizes away the .gz suffix
Claudio Sacerdoti Coen [Wed, 19 Jul 2006 09:54:03 +0000 (09:54 +0000)]
is_empty_listing fixed: the ls method normalizes away the .gz suffix

18 years agoSerious bug fixed in simplify: sometimes terms wwere not closed because of
Claudio Sacerdoti Coen [Wed, 19 Jul 2006 09:31:33 +0000 (09:31 +0000)]
Serious bug fixed in simplify: sometimes terms wwere not closed because of
the use of the wrong replace function (that did not perform the required lifting).

18 years agobaseuri for group.ma fixed
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 14:33:50 +0000 (14:33 +0000)]
baseuri for group.ma fixed

18 years agohead_beta_reduce can now optionally perform delta reduction too
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 14:30:57 +0000 (14:30 +0000)]
head_beta_reduce can now optionally perform delta reduction too

18 years agoUnification improved to handle beta-delta conversion in most cases.
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 14:30:17 +0000 (14:30 +0000)]
Unification improved to handle beta-delta conversion in most cases.
This is required to match Coq's unification for the porting of setoids.ma.

18 years agoadded split_nth
Stefano Zacchiroli [Tue, 18 Jul 2006 14:21:56 +0000 (14:21 +0000)]
added split_nth

18 years agodouble quotes node identifiers
Stefano Zacchiroli [Tue, 18 Jul 2006 14:21:04 +0000 (14:21 +0000)]
double quotes node identifiers

18 years agoBaseuri of applys.ma fixed.
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 13:58:13 +0000 (13:58 +0000)]
Baseuri of applys.ma fixed.

18 years agoQuick&dirty patch to make Http_getter_storage.is_empty ignore {.moo,.metadata.lexicon...
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 13:57:43 +0000 (13:57 +0000)]
Quick&dirty patch to make Http_getter_storage.is_empty ignore {.moo,.metadata.lexicon} files.

18 years agodependeciesParsed fixed to parse URIs also in QSTRINGs
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 13:45:08 +0000 (13:45 +0000)]
dependeciesParsed fixed to parse URIs also in QSTRINGs
(because of alias id qstring = qstring)

18 years agolegacy/coq.ma included
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 11:53:38 +0000 (11:53 +0000)]
legacy/coq.ma included

18 years agole_inv renamed to avoid conflicts with the automatically generated one.
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 11:52:51 +0000 (11:52 +0000)]
le_inv renamed to avoid conflicts with the automatically generated one.

18 years agormdir_descend now works also on non existent dirs
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 11:39:18 +0000 (11:39 +0000)]
rmdir_descend now works also on non existent dirs

18 years agomagic number incremented (because of the new declarative commands)
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 11:32:44 +0000 (11:32 +0000)]
magic number incremented (because of the new declarative commands)

18 years agolibraryclean fixed to eradicate files generated from .ma files that do not
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 11:31:34 +0000 (11:31 +0000)]
libraryclean fixed to eradicate files generated from .ma files that do not
declare any object (e.g. legacy/coq.ma)

18 years agoThe dependencies parser is more robust w.r.t. to lexing errors.
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 11:01:41 +0000 (11:01 +0000)]
The dependencies parser is more robust w.r.t. to lexing errors.

18 years ago...
Enrico Tassi [Mon, 17 Jul 2006 07:59:11 +0000 (07:59 +0000)]
...

18 years agoevvai!
Enrico Tassi [Mon, 17 Jul 2006 07:50:54 +0000 (07:50 +0000)]
evvai!

18 years ago...
Enrico Tassi [Mon, 17 Jul 2006 07:45:10 +0000 (07:45 +0000)]
...

18 years agoAdded the computation of max_weight.
Andrea Asperti [Fri, 14 Jul 2006 15:45:18 +0000 (15:45 +0000)]
Added the computation of max_weight.

18 years agoAdded the computation of max_weight for equations in proofs.
Andrea Asperti [Fri, 14 Jul 2006 15:41:26 +0000 (15:41 +0000)]
Added the computation of max_weight for equations in proofs.

18 years agoadded $Id$
Stefano Zacchiroli [Thu, 13 Jul 2006 09:41:14 +0000 (09:41 +0000)]
added $Id$

18 years agouse the graphviz pretty printer to generate graphviz markup for the coercions graph
Stefano Zacchiroli [Thu, 13 Jul 2006 09:39:51 +0000 (09:39 +0000)]
use the graphviz pretty printer to generate graphviz markup for the coercions graph

18 years agomoved graphviz pretty printer outside matita, so that it can be used by other compone...
Stefano Zacchiroli [Thu, 13 Jul 2006 09:39:17 +0000 (09:39 +0000)]
moved graphviz pretty printer outside matita, so that it can be used by other components (e.g. from CoercDb to generated coercions graph)

18 years agouse lablGraphviz to render the coercion graph and added a callback to follow hyperlin...
Stefano Zacchiroli [Wed, 12 Jul 2006 17:15:19 +0000 (17:15 +0000)]
use lablGraphviz to render the coercion graph and added a callback to follow hyperlinks there

18 years agogenerate dot files with attributes on nodes (instead of only edges), and added genera...
Stefano Zacchiroli [Wed, 12 Jul 2006 17:14:14 +0000 (17:14 +0000)]
generate dot files with attributes on nodes (instead of only edges), and added generation of the href attribute

18 years agoadded uri_of_carr
Stefano Zacchiroli [Wed, 12 Jul 2006 17:13:14 +0000 (17:13 +0000)]
added uri_of_carr

18 years agoadded pretty printer for dot files (it may need to be moved elsewhere in the future)
Stefano Zacchiroli [Wed, 12 Jul 2006 16:39:03 +0000 (16:39 +0000)]
added pretty printer for dot files (it may need to be moved elsewhere in the future)

18 years agofixed the number of columns in the clusters table
Stefano Zacchiroli [Wed, 12 Jul 2006 15:22:21 +0000 (15:22 +0000)]
fixed the number of columns in the clusters table

18 years agoDocumentation date changed.
Claudio Sacerdoti Coen [Wed, 12 Jul 2006 15:05:48 +0000 (15:05 +0000)]
Documentation date changed.

18 years agoMore commands documented.
Claudio Sacerdoti Coen [Wed, 12 Jul 2006 15:00:41 +0000 (15:00 +0000)]
More commands documented.

18 years agobugfix: remove all generated temp files
Stefano Zacchiroli [Wed, 12 Jul 2006 14:56:44 +0000 (14:56 +0000)]
bugfix: remove all generated temp files

18 years agoadded widget for rendering and interacting with graphs generated via graphviz
Stefano Zacchiroli [Wed, 12 Jul 2006 14:44:46 +0000 (14:44 +0000)]
added widget for rendering and interacting with graphs generated via graphviz

18 years agoMore commands documented.
Claudio Sacerdoti Coen [Wed, 12 Jul 2006 13:58:29 +0000 (13:58 +0000)]
More commands documented.

18 years agoMore commands documented.
Claudio Sacerdoti Coen [Wed, 12 Jul 2006 13:33:44 +0000 (13:33 +0000)]
More commands documented.

18 years agoFirst skeleton of documentation for "other commands".
Claudio Sacerdoti Coen [Wed, 12 Jul 2006 13:13:26 +0000 (13:13 +0000)]
First skeleton of documentation for "other commands".

18 years agoMissing copyright added to tactics/declarative.ml*
Claudio Sacerdoti Coen [Wed, 12 Jul 2006 12:20:18 +0000 (12:20 +0000)]
Missing copyright added to tactics/declarative.ml*

18 years agoGrafiteAst.Quit (unused) removed.
Claudio Sacerdoti Coen [Wed, 12 Jul 2006 12:19:25 +0000 (12:19 +0000)]
GrafiteAst.Quit (unused) removed.

18 years agoGrafiteAst.Print (unused) removed.
Claudio Sacerdoti Coen [Wed, 12 Jul 2006 12:13:45 +0000 (12:13 +0000)]
GrafiteAst.Print (unused) removed.

18 years agoGrafiteAst.Search_pat and GrafiteAst.Search_term (both unused) removed.
Claudio Sacerdoti Coen [Wed, 12 Jul 2006 12:09:46 +0000 (12:09 +0000)]
GrafiteAst.Search_pat and GrafiteAst.Search_term (both unused) removed.

18 years agorestored the 2 ways of pasting: both "as term" and "as pattern" are available again
Stefano Zacchiroli [Wed, 12 Jul 2006 10:43:39 +0000 (10:43 +0000)]
restored the 2 ways of pasting: both "as term" and "as pattern" are available again

18 years agoparamodulation is not a stand alone tactic: doc fixed.
Claudio Sacerdoti Coen [Wed, 12 Jul 2006 08:45:32 +0000 (08:45 +0000)]
paramodulation is not a stand alone tactic: doc fixed.

18 years agoMore documentation.
Claudio Sacerdoti Coen [Tue, 11 Jul 2006 17:18:40 +0000 (17:18 +0000)]
More documentation.

18 years agodependences updated again :)
Ferruccio Guidi [Tue, 11 Jul 2006 17:08:41 +0000 (17:08 +0000)]
dependences updated again :)

18 years agoupdated dependences
Ferruccio Guidi [Tue, 11 Jul 2006 16:52:02 +0000 (16:52 +0000)]
updated dependences

18 years agoFirst experimental version of the declarative proof language for Matita.
maiorino [Tue, 11 Jul 2006 15:44:46 +0000 (15:44 +0000)]
First experimental version of the declarative proof language for Matita.
Supported commands so far:
  assume id: term
  suppose term (id)
  by term done
  by term we proved term (id)
  we need to prove term (id)

18 years agoMore TODO items in the documentation.
Claudio Sacerdoti Coen [Tue, 11 Jul 2006 13:09:36 +0000 (13:09 +0000)]
More TODO items in the documentation.

18 years ago- removed Positive and Negative (all is positive)
Enrico Tassi [Tue, 11 Jul 2006 08:19:16 +0000 (08:19 +0000)]
- removed Positive and Negative (all is positive)
- eq_f and eq_f1 used in proofs

18 years agofixed
Enrico Tassi [Tue, 11 Jul 2006 08:06:53 +0000 (08:06 +0000)]
fixed

18 years ago...
Enrico Tassi [Mon, 10 Jul 2006 17:18:12 +0000 (17:18 +0000)]
...

18 years ago- cheanges for the new coercion stuff (including the generated graph)
Enrico Tassi [Mon, 10 Jul 2006 17:09:21 +0000 (17:09 +0000)]
- cheanges for the new coercion stuff (including the generated graph)
- new test for coercions
- new test for tinycals

18 years agorenamed the coercion
Enrico Tassi [Mon, 10 Jul 2006 17:07:49 +0000 (17:07 +0000)]
renamed the coercion

18 years agoimproved coercions support:
Enrico Tassi [Mon, 10 Jul 2006 17:07:24 +0000 (17:07 +0000)]
improved coercions support:
- multiple coercions from the same carrier are allowed
- coercions are hidden from the proof too
- a new function to print proof in text mode added

18 years agofixed 1,2: and *: according to the camera ready semantics
Enrico Tassi [Mon, 10 Jul 2006 17:04:52 +0000 (17:04 +0000)]
fixed 1,2: and *: according to the camera ready semantics

18 years agoadded flatten_map
Enrico Tassi [Mon, 10 Jul 2006 16:50:43 +0000 (16:50 +0000)]
added flatten_map

18 years agoeq_f1
Enrico Tassi [Thu, 6 Jul 2006 09:04:36 +0000 (09:04 +0000)]
eq_f1

18 years agomegatheorem (even if unused)
Enrico Tassi [Thu, 6 Jul 2006 09:04:23 +0000 (09:04 +0000)]
megatheorem (even if unused)

18 years agofixed *: and n,m:
Enrico Tassi [Thu, 6 Jul 2006 08:18:49 +0000 (08:18 +0000)]
fixed *: and n,m:

18 years ago...
Enrico Tassi [Thu, 6 Jul 2006 08:18:26 +0000 (08:18 +0000)]
...

18 years agobugfix to developments:
Enrico Tassi [Wed, 5 Jul 2006 10:40:11 +0000 (10:40 +0000)]
bugfix to developments:
- if an included .ma file is not found (not in CWD, not in include_paths)
  an error is issued
- if an included .ma file is found but the corrsponding .lexicon is not found
  a development for the .ma is searched:
  - if found it is used to compile the .ma file
  - if not found the user is aked to create a devel for the file included
    (and not the file that he is editing, that may not be in the same devel).

18 years agoInstead of closing the socket to avoid persistent connections (a bugged
Claudio Sacerdoti Coen [Mon, 3 Jul 2006 16:59:36 +0000 (16:59 +0000)]
Instead of closing the socket to avoid persistent connections (a bugged
solution in Ocaml 3.09.2), we use the new ~auto_close feature of libhttp-ocaml.

18 years agowhen auto_close is set, use flush + shutdown instead of close_out, work around an...
Stefano Zacchiroli [Mon, 3 Jul 2006 16:32:26 +0000 (16:32 +0000)]
when auto_close is set, use flush + shutdown instead of close_out, work around an ocaml 3.09.2 bug

18 years ago/....
Enrico Tassi [Mon, 3 Jul 2006 12:30:00 +0000 (12:30 +0000)]
/....