]> matita.cs.unibo.it Git - helm.git/log
helm.git
19 years agoThe file is now well formed.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:30:04 +0000 (16:30 +0000)]
The file is now well formed.

19 years agoNew syntax (again) for let rec binders:
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:19:14 +0000 (16:19 +0000)]
New syntax (again) for let rec binders:
let rec f x y (z,w:T) h (c:T) = ...

19 years agoNew lighter syntax for "let rec".
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:11:00 +0000 (16:11 +0000)]
New lighter syntax for "let rec".

19 years agoBug fixed: a symbol must be formed of just one (unicode) character.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:09:08 +0000 (16:09 +0000)]
Bug fixed: a symbol must be formed of just one (unicode) character.

19 years agoQuery results were erroneously tagged as directories.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 16:06:47 +0000 (16:06 +0000)]
Query results were erroneously tagged as directories.

19 years ago1. syntax of match changed
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 15:24:24 +0000 (15:24 +0000)]
1. syntax of match changed
2. syntax of the bindings of "let rec" made lighter

19 years agoYet another bug fixed in the inference of the outtype for match: convertibility
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 15:17:15 +0000 (15:17 +0000)]
Yet another bug fixed in the inference of the outtype for match: convertibility
was used in place of unification, making type inference much less powerful
in several useful cases.

19 years agoThe getter maps are now dumped also if matitac exits abruptly.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 14:11:02 +0000 (14:11 +0000)]
The getter maps are now dumped also if matitac exits abruptly.

19 years agoAdded new target "make tests" for regression testing.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 14:00:35 +0000 (14:00 +0000)]
Added new target "make tests" for regression testing.

19 years agoFixed a few bugs in the inference of the outtype for a match.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 13:47:53 +0000 (13:47 +0000)]
Fixed a few bugs in the inference of the outtype for a match.
In particular the instances of the left parameter that occur in the
outtype were not lifted properly because of the abstractions that correspond
to the right parameters.

19 years agoFixed inference of outtype for match when the inductive type has left and/or
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 10:52:20 +0000 (10:52 +0000)]
Fixed inference of outtype for match when the inductive type has left and/or
right parameters.

19 years agoHarder test (with empty inductive types and left and right arguments to
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 10:50:31 +0000 (10:50 +0000)]
Harder test (with empty inductive types and left and right arguments to
inductive types). It does not compile yet.

19 years agoMore informative error message.
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 10:49:49 +0000 (10:49 +0000)]
More informative error message.

19 years agoclean now also performs clean_metas (since make also creates the metas)
Claudio Sacerdoti Coen [Wed, 8 Jun 2005 09:45:59 +0000 (09:45 +0000)]
clean now also performs clean_metas (since make also creates the metas)

19 years agoadded icons to entries shown in cicbrowser so that directories are
Stefano Zacchiroli [Wed, 8 Jun 2005 09:10:17 +0000 (09:10 +0000)]
added icons to entries shown in cicbrowser so that directories are
distinguishable from objects

19 years agosnapshot (minor changes)
Stefano Zacchiroli [Wed, 8 Jun 2005 07:41:51 +0000 (07:41 +0000)]
snapshot (minor changes)

19 years ago* generate list elements in correct order
Luca Padovani [Tue, 7 Jun 2005 18:24:59 +0000 (18:24 +0000)]
* generate list elements in correct order
* handle list inside boxes
* handle box layout
* generate separator between elements (not after elements)

19 years agoadded test for coercions
Enrico Tassi [Tue, 7 Jun 2005 17:37:53 +0000 (17:37 +0000)]
added test for coercions

19 years agoadded coercions
Enrico Tassi [Tue, 7 Jun 2005 17:37:16 +0000 (17:37 +0000)]
added coercions

19 years agoimplemented attributes pretty printing
Stefano Zacchiroli [Tue, 7 Jun 2005 17:21:32 +0000 (17:21 +0000)]
implemented attributes pretty printing

19 years agohandles "elimCProp" value for class attribute
Stefano Zacchiroli [Tue, 7 Jun 2005 17:21:08 +0000 (17:21 +0000)]
handles "elimCProp" value for class attribute

19 years agoadded object attributes
Stefano Zacchiroli [Tue, 7 Jun 2005 17:20:33 +0000 (17:20 +0000)]
added object attributes

19 years agoremoved coercions from status
Enrico Tassi [Tue, 7 Jun 2005 16:43:33 +0000 (16:43 +0000)]
removed coercions from status

19 years agoadded support for coercions
Enrico Tassi [Tue, 7 Jun 2005 16:41:18 +0000 (16:41 +0000)]
added support for coercions

19 years agoadded letin
Enrico Tassi [Tue, 7 Jun 2005 16:32:41 +0000 (16:32 +0000)]
added letin

19 years agoadded syntax for letin
Enrico Tassi [Tue, 7 Jun 2005 16:32:20 +0000 (16:32 +0000)]
added syntax for letin

19 years ago1) Implemented inference of the outtype for empty inductive types
Enrico Tassi [Tue, 7 Jun 2005 15:51:43 +0000 (15:51 +0000)]
1) Implemented inference of the outtype for empty inductive types
2) The inferred outtype (of non empty ind types) used to omit the lambda abstraction (worked using an amazing feature ot the type checker meant for backward compatibility with Coq 7... ask Claudio).

19 years agochanged match syntax:
Enrico Tassi [Tue, 7 Jun 2005 15:45:19 +0000 (15:45 +0000)]
changed match syntax:
match x in type ty_x with ...

19 years agoadded whd to match argument in guarded_by_destructors;
Enrico Tassi [Tue, 7 Jun 2005 15:44:16 +0000 (15:44 +0000)]
added whd to match argument in guarded_by_destructors;
before only verbatim occurrences of safe variables were accepted.

19 years agoadded Pp of Cast
Enrico Tassi [Tue, 7 Jun 2005 15:41:09 +0000 (15:41 +0000)]
added Pp of Cast

19 years agoadded integration entry
Stefano Zacchiroli [Tue, 7 Jun 2005 15:25:11 +0000 (15:25 +0000)]
added integration entry

19 years agosnapshort
Stefano Zacchiroli [Tue, 7 Jun 2005 15:18:20 +0000 (15:18 +0000)]
snapshort
- implemented magic instantiation 2 => 1
- implemented DEFAULT pattern matching compilation 2 => 1

19 years agocontrol of dependences improved
Ferruccio Guidi [Tue, 7 Jun 2005 10:02:35 +0000 (10:02 +0000)]
control of dependences improved

19 years ago*** empty log message ***
Alberto Griggio [Tue, 7 Jun 2005 07:53:30 +0000 (07:53 +0000)]
*** empty log message ***

19 years agoMy two pennies.
Andrea Asperti [Tue, 7 Jun 2005 06:44:39 +0000 (06:44 +0000)]
My two pennies.

19 years ago- set monospace buffer using modify_font widget method
Stefano Zacchiroli [Mon, 6 Jun 2005 09:36:04 +0000 (09:36 +0000)]
- set monospace buffer using modify_font widget method
- added configuration key for user defined font and built time default

19 years ago* update
Luca Padovani [Mon, 6 Jun 2005 08:29:01 +0000 (08:29 +0000)]
* update

19 years ago* more to do
Luca Padovani [Mon, 6 Jun 2005 08:06:26 +0000 (08:06 +0000)]
* more to do

19 years ago* added todo file
Luca Padovani [Sun, 5 Jun 2005 12:32:35 +0000 (12:32 +0000)]
* added todo file

19 years agosnapshot (first version with working pattern matching both 3->2 and 2->1)
Stefano Zacchiroli [Sat, 4 Jun 2005 17:23:42 +0000 (17:23 +0000)]
snapshot (first version with working pattern matching both 3->2 and 2->1)

yupppppieeeeeeeeeeeeeeeeee!
yayyyy

19 years agoa contribution about subset theory in an intuitionistic and predicative foundation
Ferruccio Guidi [Sat, 4 Jun 2005 15:12:01 +0000 (15:12 +0000)]
a contribution about subset theory in an intuitionistic and predicative foundation

19 years agosnapshot
Stefano Zacchiroli [Sat, 4 Jun 2005 14:34:18 +0000 (14:34 +0000)]
snapshot
- regression, but better (and working!) implementation of ML pattern matching
- not yet ported 3 -> 2 pattern matching

... the dunwich horror ...

19 years agocontribution about \lambda-\delta
Ferruccio Guidi [Fri, 3 Jun 2005 21:03:39 +0000 (21:03 +0000)]
contribution about \lambda-\delta

19 years agosnapshot (added typed environment in 2 -> 1 conversion)
Stefano Zacchiroli [Thu, 2 Jun 2005 19:56:57 +0000 (19:56 +0000)]
snapshot (added typed environment in 2 -> 1 conversion)
... in the eye of the meta-vortex ...
... from Ravenna city

19 years agosnapshot (first working implementation of parttern matching from level 2
Stefano Zacchiroli [Thu, 2 Jun 2005 15:23:49 +0000 (15:23 +0000)]
snapshot (first working implementation of parttern matching from level 2
to level 1)

19 years agofix_escaping
Enrico Tassi [Wed, 1 Jun 2005 14:40:03 +0000 (14:40 +0000)]
fix_escaping

19 years agoreduce with path
Enrico Tassi [Wed, 1 Jun 2005 14:34:55 +0000 (14:34 +0000)]
reduce with path

19 years agopaths trough terms implemented with a nice hack :)
Enrico Tassi [Wed, 1 Jun 2005 14:34:36 +0000 (14:34 +0000)]
paths trough terms implemented with a nice hack :)

19 years agosome cosmetic fixes
Enrico Tassi [Wed, 1 Jun 2005 11:08:38 +0000 (11:08 +0000)]
some cosmetic fixes

19 years agofix
Enrico Tassi [Wed, 1 Jun 2005 11:06:46 +0000 (11:06 +0000)]
fix

19 years agoremoved debug prerr_endline
Enrico Tassi [Wed, 1 Jun 2005 11:06:26 +0000 (11:06 +0000)]
removed debug prerr_endline

19 years agofixed classical non-C programmer misunderstooding of pointers
Enrico Tassi [Wed, 1 Jun 2005 11:05:19 +0000 (11:05 +0000)]
fixed classical non-C programmer misunderstooding of pointers

19 years agofixed intro.
Enrico Tassi [Wed, 1 Jun 2005 11:04:22 +0000 (11:04 +0000)]
fixed intro.

19 years agoadded C.Appl [] case
Enrico Tassi [Wed, 1 Jun 2005 11:01:10 +0000 (11:01 +0000)]
added C.Appl [] case

19 years agosnapshot (ported to new "typed" ids_to_inner_sort table)
Stefano Zacchiroli [Tue, 31 May 2005 22:39:27 +0000 (22:39 +0000)]
snapshot (ported to new "typed" ids_to_inner_sort table)

19 years agoChanged type of ids_to_inner_sort table used in transformation.
Stefano Zacchiroli [Tue, 31 May 2005 22:37:56 +0000 (22:37 +0000)]
Changed type of ids_to_inner_sort table used in transformation.
It used to be (Cic.id, string) Hashtbl.t, now is (Cic.id, Cic2acic.sort_kind) Hashtbl.t where sort_kind is [ `Type | `Prop | `CProp | `Set ].
String "?", formerly used to denotes meta variable, is not mapped in sort_kind; since it was uniformly treated as "Type", `Type is now used for metas

19 years ago added comment
Enrico Tassi [Tue, 31 May 2005 15:46:15 +0000 (15:46 +0000)]
 added comment

19 years agosnapshot (first version with [apparently] working mappings between level
Stefano Zacchiroli [Tue, 31 May 2005 15:41:21 +0000 (15:41 +0000)]
snapshot (first version with [apparently] working mappings between level
2 and level 3)

19 years agoimplemented normalize (used in new_metasenv_for_apply)
Enrico Tassi [Tue, 31 May 2005 15:41:09 +0000 (15:41 +0000)]
implemented normalize (used in new_metasenv_for_apply)

19 years agofixed width fonts
Enrico Tassi [Tue, 31 May 2005 13:41:21 +0000 (13:41 +0000)]
fixed width fonts
comments

19 years agofixed comments
Enrico Tassi [Tue, 31 May 2005 13:40:59 +0000 (13:40 +0000)]
fixed comments

19 years agonew shortcuts
Enrico Tassi [Tue, 31 May 2005 13:01:29 +0000 (13:01 +0000)]
new shortcuts
fixed hint uri chooser

19 years agoadded colors
Andrea Asperti [Tue, 31 May 2005 09:54:16 +0000 (09:54 +0000)]
added colors

19 years agosnapshot (the thing on the doorstep)
Stefano Zacchiroli [Tue, 31 May 2005 09:45:45 +0000 (09:45 +0000)]
snapshot (the thing on the doorstep)

19 years agomore verbose case failure message
Andrea Asperti [Tue, 31 May 2005 09:42:30 +0000 (09:42 +0000)]
more verbose case failure message

19 years agoadded chronometer
Andrea Asperti [Tue, 31 May 2005 09:40:51 +0000 (09:40 +0000)]
added chronometer

19 years agoadded automathic aliases for _ind _rec and _rect when generated
Andrea Asperti [Tue, 31 May 2005 09:40:36 +0000 (09:40 +0000)]
added automathic aliases for _ind _rec and _rect when generated

19 years agofix
Andrea Asperti [Tue, 31 May 2005 09:40:15 +0000 (09:40 +0000)]
fix

19 years agoadded automathic aliases for qed and definition
Enrico Tassi [Tue, 31 May 2005 08:40:54 +0000 (08:40 +0000)]
added automathic aliases for qed and definition

19 years agoadded shortcuts
Enrico Tassi [Tue, 31 May 2005 08:27:21 +0000 (08:27 +0000)]
added shortcuts

19 years agofix
Enrico Tassi [Tue, 31 May 2005 08:20:54 +0000 (08:20 +0000)]
fix

19 years agoadded uri_of_term
Stefano Zacchiroli [Mon, 30 May 2005 17:14:34 +0000 (17:14 +0000)]
added uri_of_term

19 years agomah...matita.ml
Enrico Tassi [Mon, 30 May 2005 16:03:57 +0000 (16:03 +0000)]
mah...matita.ml

19 years agofix
Andrea Asperti [Mon, 30 May 2005 15:57:28 +0000 (15:57 +0000)]
fix

19 years agoadded intros n
Andrea Asperti [Mon, 30 May 2005 15:57:07 +0000 (15:57 +0000)]
added intros n

19 years agoadded intros n.
Andrea Asperti [Mon, 30 May 2005 15:56:15 +0000 (15:56 +0000)]
added intros n.

19 years agoadded automathic aliases.
Andrea Asperti [Mon, 30 May 2005 11:40:00 +0000 (11:40 +0000)]
added automathic aliases.

19 years ago- commented out no longer needed macros Redo, Undo, Abort
Stefano Zacchiroli [Fri, 27 May 2005 16:54:05 +0000 (16:54 +0000)]
- commented out no longer needed macros Redo, Undo, Abort
- bugfix: correctly handles "cic:" and "cic:/" pseudo-uris in cicBrowser
- bugfix: fixed String.sub error on directories shorted than 5 chars

19 years agofixed otags invocation
Stefano Zacchiroli [Fri, 27 May 2005 16:52:58 +0000 (16:52 +0000)]
fixed otags invocation

19 years agocommented out no longer needed macros Redo, Undo, Abort
Stefano Zacchiroli [Fri, 27 May 2005 16:52:40 +0000 (16:52 +0000)]
commented out no longer needed macros Redo, Undo, Abort

19 years agoadded %.annot rule to create type annotation files
Stefano Zacchiroli [Fri, 27 May 2005 16:52:19 +0000 (16:52 +0000)]
added %.annot rule to create type annotation files

19 years agoremoved debug prerr_endline
Enrico Tassi [Fri, 27 May 2005 16:31:47 +0000 (16:31 +0000)]
removed debug prerr_endline

19 years agofixed matitac
Enrico Tassi [Fri, 27 May 2005 16:31:18 +0000 (16:31 +0000)]
fixed matitac

19 years agorefactored modules structure
Stefano Zacchiroli [Fri, 27 May 2005 15:23:19 +0000 (15:23 +0000)]
refactored modules structure

19 years ago* fold left/right implemented
Stefano Zacchiroli [Fri, 27 May 2005 14:59:40 +0000 (14:59 +0000)]
* fold left/right implemented

19 years agosnapshot
Stefano Zacchiroli [Fri, 27 May 2005 13:20:05 +0000 (13:20 +0000)]
snapshot
- first version with working DEFAULT magic

19 years ago1. removed obsolete comments
Andrea Asperti [Fri, 27 May 2005 11:01:16 +0000 (11:01 +0000)]
1. removed obsolete comments
2. extended delift to the case of meta in head position
3. added a cases (? t1) vs t2: ? gets unified to the beta
expansion of t2 w.r.t t1.

19 years agoNow the links to 7 pages at a time are shown. Cool.
Claudio Sacerdoti Coen [Thu, 26 May 2005 16:04:05 +0000 (16:04 +0000)]
Now the links to 7 pages at a time are shown. Cool.

19 years ago256 chars max ==> 1024 chars max (because of Coq)
Claudio Sacerdoti Coen [Thu, 26 May 2005 14:52:51 +0000 (14:52 +0000)]
256 chars max ==> 1024 chars max (because of Coq)

19 years agofixed issue with explicit named substitutions
Stefano Zacchiroli [Thu, 26 May 2005 14:13:23 +0000 (14:13 +0000)]
fixed issue with explicit named substitutions

19 years agoBugs fixed:
Claudio Sacerdoti Coen [Thu, 26 May 2005 13:10:32 +0000 (13:10 +0000)]
Bugs fixed:
 1. elim did not accept identifiers with "'" in the middle
 2. elim did not accpet URIs

19 years agosnapshot
Stefano Zacchiroli [Thu, 26 May 2005 11:42:22 +0000 (11:42 +0000)]
snapshot
- first commit with working list syntax

19 years agomultiple bindings inside OPT supported
Stefano Zacchiroli [Wed, 25 May 2005 16:41:30 +0000 (16:41 +0000)]
multiple bindings inside OPT supported

19 years agobugfix: "match" now works also when no type is provided for the matched term
Stefano Zacchiroli [Wed, 25 May 2005 15:13:21 +0000 (15:13 +0000)]
bugfix: "match" now works also when no type is provided for the matched term

19 years agolet rec example
Stefano Zacchiroli [Wed, 25 May 2005 15:11:59 +0000 (15:11 +0000)]
let rec example

19 years agosnapshot (first version in which some extensions work, e.g. infix +)
Stefano Zacchiroli [Wed, 25 May 2005 14:32:40 +0000 (14:32 +0000)]
snapshot (first version in which some extensions work, e.g. infix +)
ueeeeeehh!

19 years agosome work for Gares
Ferruccio Guidi [Wed, 25 May 2005 14:16:53 +0000 (14:16 +0000)]
some work for Gares

19 years agofix
Enrico Tassi [Wed, 25 May 2005 14:02:20 +0000 (14:02 +0000)]
fix

19 years agofix
Enrico Tassi [Wed, 25 May 2005 13:46:11 +0000 (13:46 +0000)]
fix

19 years agoapply now tries both to reduce and to not reduce the applied term
Enrico Tassi [Wed, 25 May 2005 13:45:21 +0000 (13:45 +0000)]
apply now tries both to reduce and to not reduce the applied term