]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

18 years agopatched
Ferruccio Guidi [Tue, 27 Jun 2006 09:39:56 +0000 (09:39 +0000)]
patched

18 years agomore work for the generic auto parameters
Enrico Tassi [Mon, 26 Jun 2006 08:21:43 +0000 (08:21 +0000)]
more work for the generic auto parameters

18 years agoadded the geniric
Enrico Tassi [Wed, 21 Jun 2006 15:33:02 +0000 (15:33 +0000)]
added the geniric
  auto params
syntax and the auto superposition tactic

18 years agoforgotten commit
Ferruccio Guidi [Wed, 21 Jun 2006 13:20:13 +0000 (13:20 +0000)]
forgotten commit

18 years agoRELATIONAL-ARITHMETICS updated
Ferruccio Guidi [Wed, 21 Jun 2006 13:17:36 +0000 (13:17 +0000)]
RELATIONAL-ARITHMETICS updated

18 years ago- fwd concrete syntax fixed
Ferruccio Guidi [Tue, 20 Jun 2006 17:59:04 +0000 (17:59 +0000)]
- fwd concrete syntax fixed
- decompose, fwd, lapply documentation fixed

18 years agogarbage collection of dead equalities implemented
Enrico Tassi [Tue, 20 Jun 2006 12:59:42 +0000 (12:59 +0000)]
garbage collection of dead equalities implemented

18 years ago- added some documentation on the fwd tatcic
Ferruccio Guidi [Tue, 20 Jun 2006 10:51:22 +0000 (10:51 +0000)]
- added some documentation on the fwd tatcic
- lapply concrete imput syntax fixed

18 years agoPatterns are now documented.
Claudio Sacerdoti Coen [Mon, 19 Jun 2006 17:21:47 +0000 (17:21 +0000)]
Patterns are now documented.
But: how do we do multiple selections in matita?

18 years agoaxioms removed
Ferruccio Guidi [Mon, 19 Jun 2006 16:29:18 +0000 (16:29 +0000)]
axioms removed

18 years agohack to allow (**)
Ferruccio Guidi [Mon, 19 Jun 2006 16:15:24 +0000 (16:15 +0000)]
hack to allow (**)

18 years agotypo cpying the formal semantic
Enrico Tassi [Mon, 19 Jun 2006 15:51:24 +0000 (15:51 +0000)]
typo cpying the formal semantic

18 years agoreorganized guiven_clause to work with the on_the_fly simplification of goals during...
Enrico Tassi [Mon, 19 Jun 2006 15:06:39 +0000 (15:06 +0000)]
reorganized guiven_clause to work with the on_the_fly simplification of goals during ghr infer_goals step

18 years agodemodulation of goal activated again.
Enrico Tassi [Mon, 19 Jun 2006 14:44:11 +0000 (14:44 +0000)]
demodulation of goal activated again.
to deactivate it, the check_if_goal_set_us_solved should be moved after the infeer_goal step

18 years agosome experiments
Andrea Asperti [Mon, 19 Jun 2006 13:06:10 +0000 (13:06 +0000)]
some experiments

18 years agoadded (but still unused) remove_local_context
Andrea Asperti [Mon, 19 Jun 2006 13:04:18 +0000 (13:04 +0000)]
added (but still unused) remove_local_context

18 years agoadded (but not yet used) remove_local_context
Andrea Asperti [Mon, 19 Jun 2006 13:03:33 +0000 (13:03 +0000)]
added (but not yet used) remove_local_context
weight of non oriented equations decreased

18 years agoUtils.compare_terms instead of compare_weights
Andrea Asperti [Mon, 19 Jun 2006 13:01:52 +0000 (13:01 +0000)]
Utils.compare_terms instead of compare_weights
fold_right -> fold_right

18 years agooccur_check and unification fixed. now Meta(i,[]) and Meta(i,[...]) are
Andrea Asperti [Mon, 19 Jun 2006 12:58:20 +0000 (12:58 +0000)]
occur_check and unification fixed. now Meta(i,[]) and Meta(i,[...]) are
considered the same.

18 years ago...
Enrico Tassi [Mon, 19 Jun 2006 08:11:59 +0000 (08:11 +0000)]
...

18 years ago- some fixes regarding URIs of equality that now should be coherent with the
Enrico Tassi [Sun, 18 Jun 2006 12:17:18 +0000 (12:17 +0000)]
- some fixes regarding URIs of equality that now should be coherent with the
  one of the goal
- eliminated the stack overflow issue when building the proof

18 years agoinstead of including library_notation we include logic/equality that is smaller
Enrico Tassi [Sun, 18 Jun 2006 12:08:58 +0000 (12:08 +0000)]
instead of including library_notation we include logic/equality that is smaller

18 years agofix
Enrico Tassi [Sun, 18 Jun 2006 10:49:22 +0000 (10:49 +0000)]
fix

18 years agocontribution on relational arithmetics started
Ferruccio Guidi [Fri, 16 Jun 2006 20:45:00 +0000 (20:45 +0000)]
contribution on relational arithmetics started

18 years agofixed
Enrico Tassi [Fri, 16 Jun 2006 19:07:08 +0000 (19:07 +0000)]
fixed

18 years agofixes
Enrico Tassi [Fri, 16 Jun 2006 18:51:18 +0000 (18:51 +0000)]
fixes

18 years agoecco le gatte da pelare
Enrico Tassi [Fri, 16 Jun 2006 16:06:41 +0000 (16:06 +0000)]
ecco le gatte da pelare

18 years agoancient bug solved. if the term is (eq TY A B) the signature of A and B was
Enrico Tassi [Fri, 16 Jun 2006 11:51:08 +0000 (11:51 +0000)]
ancient bug solved. if the term is (eq TY A B) the signature of A and B was
ignored if TY was a Sort.

18 years agosome more on equalities
Enrico Tassi [Fri, 16 Jun 2006 11:47:25 +0000 (11:47 +0000)]
some more on equalities

18 years agoadded log.120.orsay.txt and comparison
Enrico Tassi [Fri, 16 Jun 2006 09:03:24 +0000 (09:03 +0000)]
added log.120.orsay.txt and comparison

18 years agosome examples of the new ApplyS tactic
Andrea Asperti [Thu, 15 Jun 2006 09:39:55 +0000 (09:39 +0000)]
some examples of the new ApplyS tactic

18 years agoexamples of applyS
Andrea Asperti [Thu, 15 Jun 2006 09:39:20 +0000 (09:39 +0000)]
examples of applyS

18 years agoApply-Silvie tactic added!
Andrea Asperti [Thu, 15 Jun 2006 09:38:42 +0000 (09:38 +0000)]
Apply-Silvie tactic added!

18 years agoadded applyS
Andrea Asperti [Thu, 15 Jun 2006 09:38:08 +0000 (09:38 +0000)]
added applyS

18 years agosome fixed done in Orsay:
Andrea Asperti [Thu, 15 Jun 2006 09:37:49 +0000 (09:37 +0000)]
some fixed done in Orsay:
- supL is called on both sides if the equation is not oriented
- contextualize_rewrites fixed if multiple equalities are used (equalities on different types)

18 years agoexported 2 functions needed by applyS
Andrea Asperti [Thu, 15 Jun 2006 09:35:47 +0000 (09:35 +0000)]
exported 2 functions needed by applyS

18 years ago...
Andrea Asperti [Thu, 15 Jun 2006 09:24:46 +0000 (09:24 +0000)]
...

18 years agodefault constants are now the matita standard library ones and not the one from Coq.
Andrea Asperti [Thu, 15 Jun 2006 09:22:29 +0000 (09:22 +0000)]
default constants are now the matita standard library ones and not the one from Coq.
the makefile should work on every checkout, since the path for the TPTP stuff is not hardcoded, but ppoint to the TPTP-VERSION/ directory in the user's home.

18 years agobumped date
Stefano Zacchiroli [Wed, 14 Jun 2006 15:04:13 +0000 (15:04 +0000)]
bumped date

18 years agocenter figures in HTML version of the manual using CSS
Stefano Zacchiroli [Wed, 14 Jun 2006 14:41:44 +0000 (14:41 +0000)]
center figures in HTML version of the manual using CSS

18 years agochanged install target so that figures are instaled as well
Stefano Zacchiroli [Wed, 14 Jun 2006 14:40:06 +0000 (14:40 +0000)]
changed install target so that figures are instaled as well

18 years agofixed bad spellend "stantard"
Stefano Zacchiroli [Wed, 14 Jun 2006 14:33:57 +0000 (14:33 +0000)]
fixed bad spellend "stantard"

18 years agoremoved old ignore lines about matita.conf.xml.ROLE
Stefano Zacchiroli [Wed, 14 Jun 2006 14:33:23 +0000 (14:33 +0000)]
removed old ignore lines about matita.conf.xml.ROLE

18 years agoEnrico: bugfix, remove depend.errors upon destroy
Stefano Zacchiroli [Wed, 14 Jun 2006 14:32:46 +0000 (14:32 +0000)]
Enrico: bugfix, remove depend.errors upon destroy

18 years agoremoved old debugging print
Stefano Zacchiroli [Wed, 14 Jun 2006 14:30:32 +0000 (14:30 +0000)]
removed old debugging print

18 years agorelocation of developments.png
Enrico Tassi [Wed, 14 Jun 2006 14:14:11 +0000 (14:14 +0000)]
relocation of developments.png

18 years agoadding the developments screenshot
Enrico Tassi [Wed, 14 Jun 2006 14:08:28 +0000 (14:08 +0000)]
adding the developments screenshot

18 years agobumped date
Stefano Zacchiroli [Tue, 13 Jun 2006 14:24:25 +0000 (14:24 +0000)]
bumped date

18 years agotypo: titleabbrev stuff should not be bold
Stefano Zacchiroli [Tue, 13 Jun 2006 14:22:43 +0000 (14:22 +0000)]
typo: titleabbrev stuff should not be bold

18 years agoadded generation of quick reference card of tactic syntax
Stefano Zacchiroli [Tue, 13 Jun 2006 14:18:33 +0000 (14:18 +0000)]
added generation of quick reference card of tactic syntax

18 years ago- distributed matitaGeneratedGui.ml (needed)
Stefano Zacchiroli [Tue, 13 Jun 2006 12:03:51 +0000 (12:03 +0000)]
- distributed matitaGeneratedGui.ml (needed)
- when distributed 'world' is the default target

18 years agogenerate gui code upon distribution
Stefano Zacchiroli [Tue, 13 Jun 2006 11:42:28 +0000 (11:42 +0000)]
generate gui code upon distribution

18 years agodistribute more stuff
Stefano Zacchiroli [Tue, 13 Jun 2006 10:21:57 +0000 (10:21 +0000)]
distribute more stuff
added an install target to the manual makefile

18 years agoreordered author list
Stefano Zacchiroli [Tue, 13 Jun 2006 10:21:28 +0000 (10:21 +0000)]
reordered author list