]> matita.cs.unibo.it Git - helm.git/log
helm.git
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 agooutput headers to force utf-8 charset
Stefano Zacchiroli [Tue, 18 Jul 2006 08:47:58 +0000 (08:47 +0000)]
output headers to force utf-8 charset

18 years agochanged colors to match our GtkSourceView settings
Stefano Zacchiroli [Tue, 18 Jul 2006 08:47:41 +0000 (08:47 +0000)]
changed colors to match our GtkSourceView settings

18 years agoreal life implementation of the highlighting, added css
Stefano Zacchiroli [Mon, 17 Jul 2006 09:49:44 +0000 (09:49 +0000)]
real life implementation of the highlighting, added css

18 years ago- added format table (enable highlighting of differente file formats)
Stefano Zacchiroli [Mon, 17 Jul 2006 09:49:29 +0000 (09:49 +0000)]
- added format table (enable highlighting of differente file formats)
- enclosed highlighted body in <pre> .. </pre>
- added reference to the used .css

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 agoproof of concept implementation of scripts highlighting, grafite.hrc is still bugged
Stefano Zacchiroli [Fri, 14 Jul 2006 12:54:10 +0000 (12:54 +0000)]
proof of concept implementation of scripts highlighting, grafite.hrc is still bugged

18 years agosnapshot
Stefano Zacchiroli [Fri, 14 Jul 2006 12:06:30 +0000 (12:06 +0000)]
snapshot

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)]
/....

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

18 years ago- patch to consider the symbols of the goal when computing the weight of an
Enrico Tassi [Mon, 3 Jul 2006 11:48:44 +0000 (11:48 +0000)]
- patch to consider the symbols of the goal when computing the weight of an
  equality.
- actives simplified during fwd/back are not appended (but put in front) of the
  passive list

18 years agoDocumentation of tinycals started.
Claudio Sacerdoti Coen [Fri, 30 Jun 2006 16:39:28 +0000 (16:39 +0000)]
Documentation of tinycals started.

18 years agopretty proofs are back
Enrico Tassi [Fri, 30 Jun 2006 15:52:18 +0000 (15:52 +0000)]
pretty proofs are back

18 years agofix
Enrico Tassi [Fri, 30 Jun 2006 12:37:33 +0000 (12:37 +0000)]
fix

18 years ago"linear" keyword inserted (used by lapply)
Ferruccio Guidi [Thu, 29 Jun 2006 14:23:41 +0000 (14:23 +0000)]
"linear" keyword inserted (used by lapply)

18 years agoCleaning up; removed a couple of "open".
Andrea Asperti [Thu, 29 Jun 2006 13:38:14 +0000 (13:38 +0000)]
Cleaning up; removed a couple of "open".

18 years ago...
Enrico Tassi [Thu, 29 Jun 2006 11:30:44 +0000 (11:30 +0000)]
...

18 years agoDemodulate used to be a reduction_kind and it used to take a ~pattern.
Claudio Sacerdoti Coen [Thu, 29 Jun 2006 11:27:35 +0000 (11:27 +0000)]
Demodulate used to be a reduction_kind and it used to take a ~pattern.
Since demodulation is not a reduction kind, I changed it to a normal tactic.
Moreover, since the ~pattern was unused, I have temporarily removed it.
Doc changed accordingly.

18 years agoWORK IN PROGRESS:
Claudio Sacerdoti Coen [Thu, 29 Jun 2006 11:19:20 +0000 (11:19 +0000)]
WORK IN PROGRESS:
First commit of setoids.ml* (a porting from the Coq code by Claudio Sacerdoti
Coen).
The file setoids.ml is now compiled (and linked), but it does not provide any
functionality yet.
"(*Coq" comments are used in several places for parts of the code not ported
to Matita yet.

18 years agobefore goals are inferred with current,
Enrico Tassi [Thu, 29 Jun 2006 11:17:46 +0000 (11:17 +0000)]
before goals are inferred with current,
we demodulate them with active+current
(was: only with current)

18 years agoDocumentation for variant fixed (the type and body are NOT optional).
Claudio Sacerdoti Coen [Thu, 29 Jun 2006 10:53:30 +0000 (10:53 +0000)]
Documentation for variant fixed (the type and body are NOT optional).

18 years agogoals after a superposition step are relocated
Enrico Tassi [Thu, 29 Jun 2006 10:01:16 +0000 (10:01 +0000)]
goals after a superposition step are relocated

18 years ago- "linear" flag added to lapply (automatic clearing)
Ferruccio Guidi [Wed, 28 Jun 2006 17:24:38 +0000 (17:24 +0000)]
- "linear" flag added to lapply (automatic clearing)
- RELATIONAL-ARITHMETICS updated to use this flag

18 years agokarma: every term the rewrite acts on must be substututed
Enrico Tassi [Wed, 28 Jun 2006 14:39:58 +0000 (14:39 +0000)]
karma: every term the rewrite acts on must be substututed

18 years agofix
Enrico Tassi [Wed, 28 Jun 2006 12:45:06 +0000 (12:45 +0000)]
fix

18 years agofix
Enrico Tassi [Wed, 28 Jun 2006 10:34:19 +0000 (10:34 +0000)]
fix

18 years agofix
Enrico Tassi [Wed, 28 Jun 2006 10:31:44 +0000 (10:31 +0000)]
fix

18 years agofixed gzip usage
Enrico Tassi [Wed, 28 Jun 2006 10:29:57 +0000 (10:29 +0000)]
fixed gzip usage

18 years agosuperposition_left not performed if the input goal is an identity
Enrico Tassi [Wed, 28 Jun 2006 10:28:58 +0000 (10:28 +0000)]
superposition_left not performed if the input goal is an identity

18 years agofix
Enrico Tassi [Wed, 28 Jun 2006 10:28:13 +0000 (10:28 +0000)]
fix

18 years agocsc trick on steroids
Enrico Tassi [Wed, 28 Jun 2006 09:02:56 +0000 (09:02 +0000)]
csc trick on steroids

18 years agonew mega spreadsheet available
Enrico Tassi [Wed, 28 Jun 2006 08:11:22 +0000 (08:11 +0000)]
new mega spreadsheet available

18 years agofix
Enrico Tassi [Wed, 28 Jun 2006 08:06:53 +0000 (08:06 +0000)]
fix

18 years agoadded gzip to log files
Enrico Tassi [Wed, 28 Jun 2006 08:06:34 +0000 (08:06 +0000)]
added gzip to log files

18 years ago- decompose now runs with no arguments (operates on the whole context)
Ferruccio Guidi [Tue, 27 Jun 2006 16:57:46 +0000 (16:57 +0000)]
- decompose now runs with no arguments (operates on the whole context)
- clear now takes a list of hypotheses (clears each)
- RELATIONAL-ARITHMETICS updated to use the new tactics
- tactics/Makefile fixed to correctly build tactics.mli

18 years agofixed infer_goal, added simplification before inferring with current
Enrico Tassi [Tue, 27 Jun 2006 16:55:52 +0000 (16:55 +0000)]
fixed infer_goal, added simplification before inferring with current

18 years agousing the new metadataConstraint function
Enrico Tassi [Tue, 27 Jun 2006 16:54:28 +0000 (16:54 +0000)]
using the new metadataConstraint function

18 years agoused the new metadataConstraint function to retrieve equalities from the library
Enrico Tassi [Tue, 27 Jun 2006 16:53:48 +0000 (16:53 +0000)]
used the new metadataConstraint function to retrieve equalities from the library

18 years agofixed equalities_for_goal
Enrico Tassi [Tue, 27 Jun 2006 16:52:45 +0000 (16:52 +0000)]
fixed equalities_for_goal

18 years agothe old compute_eq_weight is back (no more max)
Enrico Tassi [Tue, 27 Jun 2006 16:49:29 +0000 (16:49 +0000)]
the old compute_eq_weight is back (no more max)

18 years agofixed generation of letins
Enrico Tassi [Tue, 27 Jun 2006 16:47:15 +0000 (16:47 +0000)]
fixed generation of letins

18 years agoadded a metas_of_term implemented using sets instead of lists (avoids some stack...
Enrico Tassi [Tue, 27 Jun 2006 16:44:14 +0000 (16:44 +0000)]
added a metas_of_term implemented using sets instead of lists (avoids some stack overflows)

18 years agofile names patched
Ferruccio Guidi [Tue, 27 Jun 2006 09:40:34 +0000 (09:40 +0000)]
file names patched