]>
matita.cs.unibo.it Git - helm.git/log
Ferruccio Guidi [Fri, 10 May 2013 16:19:46 +0000 (16:19 +0000)]
partial update in basic_2 ...
Ferruccio Guidi [Fri, 10 May 2013 16:15:53 +0000 (16:15 +0000)]
- partial commit: we issue the "conversion" and "equivalence" components
- we park conversion and equivalence on local environments for the moment
Ferruccio Guidi [Thu, 9 May 2013 20:55:35 +0000 (20:55 +0000)]
partial commit in basic_2
Ferruccio Guidi [Thu, 9 May 2013 20:53:51 +0000 (20:53 +0000)]
partial commit: finaly we issue the "computation" component ...
Ferruccio Guidi [Tue, 7 May 2013 16:07:42 +0000 (16:07 +0000)]
- partial commit: refactoring in the components before "computation"
Ferruccio Guidi [Sun, 5 May 2013 18:25:54 +0000 (18:25 +0000)]
partial update in basic_2
Ferruccio Guidi [Sun, 5 May 2013 18:16:14 +0000 (18:16 +0000)]
- partial commit (just the components before computation)
- we park head normal forms for the moment
- some refactoring
Andrea Asperti [Fri, 3 May 2013 06:51:37 +0000 (06:51 +0000)]
reverse complexity
Claudio Sacerdoti Coen [Tue, 30 Apr 2013 17:05:53 +0000 (17:05 +0000)]
Bumped to 0.99.2.
Claudio Sacerdoti Coen [Tue, 30 Apr 2013 17:05:36 +0000 (17:05 +0000)]
Missing include.
Andrea Asperti [Tue, 30 Apr 2013 16:17:51 +0000 (16:17 +0000)]
chapter9
Andrea Asperti [Tue, 30 Apr 2013 16:15:46 +0000 (16:15 +0000)]
tutorial
Claudio Sacerdoti Coen [Tue, 30 Apr 2013 16:05:01 +0000 (16:05 +0000)]
Old version dropped.
Andrea Asperti [Tue, 30 Apr 2013 15:53:37 +0000 (15:53 +0000)]
New notation for congruence
Andrea Asperti [Tue, 30 Apr 2013 15:39:19 +0000 (15:39 +0000)]
This line, and those below, will be ignored--
M chebyshev/chebyshev_psi.ma
D chebyshev/chebyshev_B.ma
matitaweb [Tue, 30 Apr 2013 14:51:34 +0000 (14:51 +0000)]
commit by user ricciott
Andrea Asperti [Mon, 29 Apr 2013 09:57:24 +0000 (09:57 +0000)]
A few integrations (closed an axiom in finset).
matitaweb [Sat, 27 Apr 2013 15:56:10 +0000 (15:56 +0000)]
commit by user andrea
matitaweb [Sat, 27 Apr 2013 15:00:47 +0000 (15:00 +0000)]
commit by user andrea
matitaweb [Sat, 27 Apr 2013 14:59:25 +0000 (14:59 +0000)]
commit by user andrea
matitaweb [Sat, 27 Apr 2013 14:49:38 +0000 (14:49 +0000)]
commit by user andrea
matitaweb [Fri, 26 Apr 2013 16:09:28 +0000 (16:09 +0000)]
commit by user andrea
Wilmer Ricciotti [Thu, 25 Apr 2013 07:15:53 +0000 (07:15 +0000)]
An attempt at ostensiby named syntax.
Ferruccio Guidi [Sun, 21 Apr 2013 15:53:55 +0000 (15:53 +0000)]
update in basic_2
Ferruccio Guidi [Sun, 21 Apr 2013 15:52:11 +0000 (15:52 +0000)]
one file was missing
Ferruccio Guidi [Sun, 21 Apr 2013 15:51:01 +0000 (15:51 +0000)]
- we commit the "reduction" component
- we park the focalized reduction for the moment
- some refactoring
Ferruccio Guidi [Sat, 20 Apr 2013 19:34:58 +0000 (19:34 +0000)]
update in basic_2
Ferruccio Guidi [Sat, 20 Apr 2013 18:27:28 +0000 (18:27 +0000)]
refactoring should be completed now
Ferruccio Guidi [Sat, 20 Apr 2013 18:24:54 +0000 (18:24 +0000)]
refactoring completed :)
Ferruccio Guidi [Sat, 20 Apr 2013 18:21:31 +0000 (18:21 +0000)]
- we are committing just the components before "reducibility"
- first definition of "unfold"
- notation bugfix
- some refactoring
matitaweb [Fri, 19 Apr 2013 18:38:02 +0000 (18:38 +0000)]
commit by user lroversi
matitaweb [Wed, 17 Apr 2013 11:12:29 +0000 (11:12 +0000)]
commit by user andrea
Wilmer Ricciotti [Wed, 17 Apr 2013 10:50:45 +0000 (10:50 +0000)]
Fixes a bug which caused Meta_not_found exceptions to be raised after qed-ing a
lemma with unskipped goals closed by side-effect.
Ferruccio Guidi [Tue, 16 Apr 2013 19:52:17 +0000 (19:52 +0000)]
milestone update in basic_2!
Ferruccio Guidi [Tue, 16 Apr 2013 19:45:41 +0000 (19:45 +0000)]
- we commit just the components before "reducibility"
- reaxiomatized substitution and reduction now commute with respect to
subclosure
- delift and thin removed for now
Ferruccio Guidi [Mon, 15 Apr 2013 17:55:59 +0000 (17:55 +0000)]
uncommited file found :)
matitaweb [Wed, 10 Apr 2013 11:44:22 +0000 (11:44 +0000)]
commit by user andrea
matitaweb [Wed, 10 Apr 2013 11:43:43 +0000 (11:43 +0000)]
commit by user andrea
matitaweb [Wed, 10 Apr 2013 11:32:54 +0000 (11:32 +0000)]
commit by user andrea
matitaweb [Wed, 10 Apr 2013 10:01:59 +0000 (10:01 +0000)]
commit by user andrea
Wilmer Ricciotti [Tue, 9 Apr 2013 13:41:15 +0000 (13:41 +0000)]
Fixes a bug that caused an assertion failure when no notation was defined.
Claudio Sacerdoti Coen [Mon, 8 Apr 2013 12:20:15 +0000 (12:20 +0000)]
Patch by Paolo Tranquilli. It fixes the following problem: when a new
tab was openened, the interface got confused about which script was focused.
It did not save the previous focused script if it was at end of file and
it saved it instead when switching from the new tab. Other bugs could be related
to that.
matitaweb [Mon, 8 Apr 2013 11:53:15 +0000 (11:53 +0000)]
commit by user andrea
Ferruccio Guidi [Sun, 7 Apr 2013 21:38:03 +0000 (21:38 +0000)]
update in basic_2 and apps_2
Ferruccio Guidi [Sun, 7 Apr 2013 21:36:03 +0000 (21:36 +0000)]
- new component for restricted computation (delta, zeta and tau only)
- subclosure preseves native validity asexpected
- some renaming
Ferruccio Guidi [Fri, 5 Apr 2013 12:25:17 +0000 (12:25 +0000)]
update in basic_2
Ferruccio Guidi [Fri, 5 Apr 2013 11:56:45 +0000 (11:56 +0000)]
- parallel substitution reaxiomatized
- supclosure reaxiomatixed (now commutes with parallel substitution)
- some refactoring
Ferruccio Guidi [Wed, 20 Mar 2013 18:43:07 +0000 (18:43 +0000)]
- probe: recursive removal of empty directories
- matitadep: improved parsing of input
Ferruccio Guidi [Mon, 18 Mar 2013 21:03:54 +0000 (21:03 +0000)]
missing or rootless dependences now don't break the compilation process
Ferruccio Guidi [Mon, 18 Mar 2013 19:28:47 +0000 (19:28 +0000)]
some additions
Ferruccio Guidi [Mon, 18 Mar 2013 19:23:53 +0000 (19:23 +0000)]
update in basic_2
Ferruccio Guidi [Mon, 18 Mar 2013 19:21:57 +0000 (19:21 +0000)]
a file was added by mistake
Ferruccio Guidi [Mon, 18 Mar 2013 19:10:19 +0000 (19:10 +0000)]
- more understanding of the "big tree" reduction step
Ferruccio Guidi [Sun, 17 Mar 2013 23:31:36 +0000 (23:31 +0000)]
sfr renamed as lbotr and its symbol changed according to lsubr
Ferruccio Guidi [Sun, 17 Mar 2013 19:51:19 +0000 (19:51 +0000)]
notational change for lsubr:
now looks like the other refinements for local environments
Ferruccio Guidi [Sun, 17 Mar 2013 17:43:13 +0000 (17:43 +0000)]
lsubs renamed as lsubr
Ferruccio Guidi [Sun, 17 Mar 2013 15:28:18 +0000 (15:28 +0000)]
notational change for snv and lsubsv: inverted "!" used for now
Ferruccio Guidi [Sat, 16 Mar 2013 22:28:17 +0000 (22:28 +0000)]
milestone in basic_2!
Ferruccio Guidi [Sat, 16 Mar 2013 22:24:19 +0000 (22:24 +0000)]
- lambdadelta: last recursive part of preservation finally proved!
some notational changes
- BTM: one file was missing
- probe: now sources and objects not having a .ma file are deleted
Ferruccio Guidi [Thu, 14 Mar 2013 23:12:55 +0000 (23:12 +0000)]
this is the real update :)
Ferruccio Guidi [Thu, 14 Mar 2013 23:07:40 +0000 (23:07 +0000)]
update in basic_2
Ferruccio Guidi [Thu, 14 Mar 2013 23:06:19 +0000 (23:06 +0000)]
- main proof case closed in the 4th component of preservation
- bug fix in Makefile: now both xoa and probe receive both
configuration files
- useless notion lsubss removed (to be replaced by lsubse)
Ferruccio Guidi [Wed, 13 Mar 2013 22:11:34 +0000 (22:11 +0000)]
- lambdadelta: third recursive part of preservation finally proved!
Makefile: xoa.conf passed to probe for future use
- xoa, probe: now can *really* take several configuration files
Ferruccio Guidi [Mon, 11 Mar 2013 19:29:23 +0000 (19:29 +0000)]
more results on lenv refinement for stratified native validity
Ferruccio Guidi [Mon, 11 Mar 2013 19:27:07 +0000 (19:27 +0000)]
bugfix in web tables
Ferruccio Guidi [Mon, 11 Mar 2013 19:21:15 +0000 (19:21 +0000)]
some bugs fixed
Ferruccio Guidi [Mon, 11 Mar 2013 12:59:19 +0000 (12:59 +0000)]
- xslt and Makefile improved, web pages regenerated
Andrea Asperti [Mon, 11 Mar 2013 10:32:22 +0000 (10:32 +0000)]
Chpater 4 and 5
Ferruccio Guidi [Sun, 10 Mar 2013 17:05:30 +0000 (17:05 +0000)]
- improved Makefile esp. with the "trim" function
- some files trimmed
Andrea Asperti [Sun, 10 Mar 2013 14:08:14 +0000 (14:08 +0000)]
chapters 2 e 3
Ferruccio Guidi [Sun, 10 Mar 2013 12:01:43 +0000 (12:01 +0000)]
we removed a useless assertion that was forcing matita to edit just matita files
matita's editor is good on its own and has interesting facilities including predefined virtuals
in lambdadelta we use matita to edit the .tbl files containing notation from the .ma's
and we use matita as well to edit predefined_virtuals.ml
we still wonder how we could do this up to now despite the assertion!
Ferruccio Guidi [Sat, 9 Mar 2013 22:32:07 +0000 (22:32 +0000)]
- update in basic_2
- contrib specific web pages moved out
- improved Makefiles
Ferruccio Guidi [Sat, 9 Mar 2013 22:26:54 +0000 (22:26 +0000)]
basic_2_src.tbl was not updated :(
Ferruccio Guidi [Sat, 9 Mar 2013 17:14:31 +0000 (17:14 +0000)]
- lenv refinement for stratified native validity redefined
- contrib specufic web pages moved here
Ferruccio Guidi [Fri, 8 Mar 2013 19:48:14 +0000 (19:48 +0000)]
second recursive part of preservation finally proved!
Ferruccio Guidi [Fri, 8 Mar 2013 13:47:28 +0000 (13:47 +0000)]
update in basic_2
Ferruccio Guidi [Fri, 8 Mar 2013 13:33:29 +0000 (13:33 +0000)]
improved "big treee" computation allows to close a case in the
preservation proof
Claudio Sacerdoti Coen [Mon, 4 Mar 2013 01:31:00 +0000 (01:31 +0000)]
Bug fixed: let-rec defined propositions are no longer extracted.
They used to be extracted, but in the interface the type abstraction was
wrong.
Ferruccio Guidi [Sun, 3 Mar 2013 18:54:10 +0000 (18:54 +0000)]
update in basic_2
Ferruccio Guidi [Sun, 3 Mar 2013 18:52:14 +0000 (18:52 +0000)]
- lambdadelta: we removed focalized reduction from snv preservation
- matitadep: bug fix in loop detection
Ferruccio Guidi [Thu, 28 Feb 2013 18:15:19 +0000 (18:15 +0000)]
update in basic_2
Ferruccio Guidi [Thu, 28 Feb 2013 18:14:27 +0000 (18:14 +0000)]
- lambdadelta: first recursive part of preservation finally proved!
- lambda: bugfix in include paths, now they are relative to the root
- matita.lang: keyword "fact" added (used in lambdadelta)
Andrea Asperti [Thu, 28 Feb 2013 16:22:28 +0000 (16:22 +0000)]
chapter2 revisited
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:19:28 +0000 (20:19 +0000)]
Quick patch: the maxmeta is now pushed/popped when compiling an external file.
This is implemented imperatively for now. It should go into a status.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:19:04 +0000 (20:19 +0000)]
Quick patch: the maxmeta is now pushed/popped when compiling an external file.
This is implemented imperatively for now. It should go into a status.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:18:18 +0000 (20:18 +0000)]
Bug fixed: composite coercions were not extracted.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:17:41 +0000 (20:17 +0000)]
Bug fixed that reveals a new one: in case of inductive types defined via
let rec, it used to happen that a "type 'a foo" in the .mli was implemented
by a "type 'a foo" in the .ml. Now the opposite happens in other situations.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 18:30:24 +0000 (18:30 +0000)]
Ferruccio's removal of objects commented out because it breaks compilation of
the standard library!
Andrea Asperti [Wed, 27 Feb 2013 16:48:15 +0000 (16:48 +0000)]
Chapter 1 revisited
Ferruccio Guidi [Mon, 25 Feb 2013 21:22:24 +0000 (21:22 +0000)]
when we serialize the contents of a .ma, we remove the old objects
before adding the new ones
Ferruccio Guidi [Sun, 24 Feb 2013 18:25:57 +0000 (18:25 +0000)]
- xhtbl: now double quotes can appear in string literals
built-in help completed
Ferruccio Guidi [Sun, 24 Feb 2013 16:20:34 +0000 (16:20 +0000)]
- nUri : added Sets of uris for use in "probe"
- probe: now we can exclude the objects of dismissed sources
(those in .matita/ but not in the development as .ma)
- lambdadelta: Makefile now uses the new feature of "probe"
Ferruccio Guidi [Fri, 22 Feb 2013 21:54:29 +0000 (21:54 +0000)]
update in basic_2
Ferruccio Guidi [Fri, 22 Feb 2013 21:47:07 +0000 (21:47 +0000)]
- "big tree" order implemented
- some annotations
Ferruccio Guidi [Mon, 18 Feb 2013 21:50:27 +0000 (21:50 +0000)]
trace added in a failing invocation of auto :-(
Ferruccio Guidi [Mon, 18 Feb 2013 19:41:43 +0000 (19:41 +0000)]
update in basic_2
Ferruccio Guidi [Mon, 18 Feb 2013 19:40:13 +0000 (19:40 +0000)]
substitution lemma for stratified native validity!
Ferruccio Guidi [Fri, 15 Feb 2013 18:54:16 +0000 (18:54 +0000)]
update in basic_2 summary
Ferruccio Guidi [Fri, 15 Feb 2013 18:52:30 +0000 (18:52 +0000)]
we rephrased sstas in terms of star
Ferruccio Guidi [Fri, 15 Feb 2013 14:21:51 +0000 (14:21 +0000)]
update in basic_2