]> matita.cs.unibo.it Git - helm.git/log
helm.git
11 years agopartial update in basic_2 ...
Ferruccio Guidi [Fri, 10 May 2013 16:19:46 +0000 (16:19 +0000)]
partial update in basic_2 ...

11 years ago- partial commit: we issue the "conversion" and "equivalence" components
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

11 years agopartial commit in basic_2
Ferruccio Guidi [Thu, 9 May 2013 20:55:35 +0000 (20:55 +0000)]
partial commit in basic_2

11 years agopartial commit: finaly we issue the "computation" component ...
Ferruccio Guidi [Thu, 9 May 2013 20:53:51 +0000 (20:53 +0000)]
partial commit: finaly we issue the "computation" component ...

11 years ago- partial commit: refactoring in the components before "computation"
Ferruccio Guidi [Tue, 7 May 2013 16:07:42 +0000 (16:07 +0000)]
- partial commit: refactoring in the components before "computation"

11 years agopartial update in basic_2
Ferruccio Guidi [Sun, 5 May 2013 18:25:54 +0000 (18:25 +0000)]
partial update in basic_2

11 years ago- partial commit (just the components before computation)
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

11 years agoreverse complexity
Andrea Asperti [Fri, 3 May 2013 06:51:37 +0000 (06:51 +0000)]
reverse complexity

11 years agoBumped to 0.99.2.
Claudio Sacerdoti Coen [Tue, 30 Apr 2013 17:05:53 +0000 (17:05 +0000)]
Bumped to 0.99.2.

11 years agoMissing include.
Claudio Sacerdoti Coen [Tue, 30 Apr 2013 17:05:36 +0000 (17:05 +0000)]
Missing include.

11 years agochapter9
Andrea Asperti [Tue, 30 Apr 2013 16:17:51 +0000 (16:17 +0000)]
chapter9

11 years agotutorial
Andrea Asperti [Tue, 30 Apr 2013 16:15:46 +0000 (16:15 +0000)]
tutorial

11 years agoOld version dropped.
Claudio Sacerdoti Coen [Tue, 30 Apr 2013 16:05:01 +0000 (16:05 +0000)]
Old version dropped.

11 years agoNew notation for congruence
Andrea Asperti [Tue, 30 Apr 2013 15:53:37 +0000 (15:53 +0000)]
New notation for congruence

11 years agoThis line, and those below, will be ignored--
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

11 years agocommit by user ricciott
matitaweb [Tue, 30 Apr 2013 14:51:34 +0000 (14:51 +0000)]
commit by user ricciott

11 years agoA few integrations (closed an axiom in finset).
Andrea Asperti [Mon, 29 Apr 2013 09:57:24 +0000 (09:57 +0000)]
A few integrations (closed an axiom in finset).

11 years agocommit by user andrea
matitaweb [Sat, 27 Apr 2013 15:56:10 +0000 (15:56 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Sat, 27 Apr 2013 15:00:47 +0000 (15:00 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Sat, 27 Apr 2013 14:59:25 +0000 (14:59 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Sat, 27 Apr 2013 14:49:38 +0000 (14:49 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Fri, 26 Apr 2013 16:09:28 +0000 (16:09 +0000)]
commit by user andrea

11 years agoAn attempt at ostensiby named syntax.
Wilmer Ricciotti [Thu, 25 Apr 2013 07:15:53 +0000 (07:15 +0000)]
An attempt at ostensiby named syntax.

11 years agoupdate in basic_2
Ferruccio Guidi [Sun, 21 Apr 2013 15:53:55 +0000 (15:53 +0000)]
update in basic_2

11 years agoone file was missing
Ferruccio Guidi [Sun, 21 Apr 2013 15:52:11 +0000 (15:52 +0000)]
one file was missing

11 years ago- we commit the "reduction" component
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

11 years agoupdate in basic_2
Ferruccio Guidi [Sat, 20 Apr 2013 19:34:58 +0000 (19:34 +0000)]
update in basic_2

11 years agorefactoring should be completed now
Ferruccio Guidi [Sat, 20 Apr 2013 18:27:28 +0000 (18:27 +0000)]
refactoring should be completed now

11 years agorefactoring completed :)
Ferruccio Guidi [Sat, 20 Apr 2013 18:24:54 +0000 (18:24 +0000)]
refactoring completed :)

11 years ago- we are committing just the components before "reducibility"
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

11 years agocommit by user lroversi
matitaweb [Fri, 19 Apr 2013 18:38:02 +0000 (18:38 +0000)]
commit by user lroversi

11 years agocommit by user andrea
matitaweb [Wed, 17 Apr 2013 11:12:29 +0000 (11:12 +0000)]
commit by user andrea

11 years agoFixes a bug which caused Meta_not_found exceptions to be raised after qed-ing a
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.

11 years agomilestone update in basic_2!
Ferruccio Guidi [Tue, 16 Apr 2013 19:52:17 +0000 (19:52 +0000)]
milestone update in basic_2!

11 years ago- we commit just the components before "reducibility"
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

11 years agouncommited file found :)
Ferruccio Guidi [Mon, 15 Apr 2013 17:55:59 +0000 (17:55 +0000)]
uncommited file found :)

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 11:44:22 +0000 (11:44 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 11:43:43 +0000 (11:43 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 11:32:54 +0000 (11:32 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 10:01:59 +0000 (10:01 +0000)]
commit by user andrea

11 years agoFixes a bug that caused an assertion failure when no notation was defined.
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.

11 years agoPatch by Paolo Tranquilli. It fixes the following problem: when a new
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.

11 years agocommit by user andrea
matitaweb [Mon, 8 Apr 2013 11:53:15 +0000 (11:53 +0000)]
commit by user andrea

11 years agoupdate in basic_2 and apps_2
Ferruccio Guidi [Sun, 7 Apr 2013 21:38:03 +0000 (21:38 +0000)]
update in basic_2 and apps_2

11 years ago- new component for restricted computation (delta, zeta and tau only)
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

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 5 Apr 2013 12:25:17 +0000 (12:25 +0000)]
update in basic_2

11 years ago- parallel substitution reaxiomatized
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

11 years ago- probe: recursive removal of empty directories
Ferruccio Guidi [Wed, 20 Mar 2013 18:43:07 +0000 (18:43 +0000)]
- probe: recursive removal of empty directories
- matitadep: improved parsing of input

11 years agomissing or rootless dependences now don't break the compilation process
Ferruccio Guidi [Mon, 18 Mar 2013 21:03:54 +0000 (21:03 +0000)]
missing or rootless dependences now don't break the compilation process

11 years agosome additions
Ferruccio Guidi [Mon, 18 Mar 2013 19:28:47 +0000 (19:28 +0000)]
some additions

11 years agoupdate in basic_2
Ferruccio Guidi [Mon, 18 Mar 2013 19:23:53 +0000 (19:23 +0000)]
update in basic_2

11 years agoa file was added by mistake
Ferruccio Guidi [Mon, 18 Mar 2013 19:21:57 +0000 (19:21 +0000)]
a file was added by mistake

11 years ago- more understanding of the "big tree" reduction step
Ferruccio Guidi [Mon, 18 Mar 2013 19:10:19 +0000 (19:10 +0000)]
- more understanding of the "big tree" reduction step

11 years agosfr renamed as lbotr and its symbol changed according to lsubr
Ferruccio Guidi [Sun, 17 Mar 2013 23:31:36 +0000 (23:31 +0000)]
sfr renamed as lbotr and its symbol changed according to lsubr

11 years agonotational change for 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

11 years agolsubs renamed as lsubr
Ferruccio Guidi [Sun, 17 Mar 2013 17:43:13 +0000 (17:43 +0000)]
lsubs renamed as lsubr

11 years agonotational change for snv and lsubsv: inverted "!" used for now
Ferruccio Guidi [Sun, 17 Mar 2013 15:28:18 +0000 (15:28 +0000)]
notational change for snv and lsubsv: inverted "!" used for now

11 years agomilestone in basic_2!
Ferruccio Guidi [Sat, 16 Mar 2013 22:28:17 +0000 (22:28 +0000)]
milestone in basic_2!

11 years ago- lambdadelta: last recursive part of preservation finally proved!
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

11 years agothis is the real update :)
Ferruccio Guidi [Thu, 14 Mar 2013 23:12:55 +0000 (23:12 +0000)]
this is the real update :)

11 years agoupdate in basic_2
Ferruccio Guidi [Thu, 14 Mar 2013 23:07:40 +0000 (23:07 +0000)]
update in basic_2

11 years ago- main proof case closed in the 4th component of preservation
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)

11 years ago- lambdadelta: third recursive part of preservation finally proved!
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

11 years agomore results on lenv refinement for stratified native validity
Ferruccio Guidi [Mon, 11 Mar 2013 19:29:23 +0000 (19:29 +0000)]
more results on lenv refinement for stratified native validity

11 years agobugfix in web tables
Ferruccio Guidi [Mon, 11 Mar 2013 19:27:07 +0000 (19:27 +0000)]
bugfix in web tables

11 years agosome bugs fixed
Ferruccio Guidi [Mon, 11 Mar 2013 19:21:15 +0000 (19:21 +0000)]
some bugs fixed

11 years ago- xslt and Makefile improved, web pages regenerated
Ferruccio Guidi [Mon, 11 Mar 2013 12:59:19 +0000 (12:59 +0000)]
- xslt and Makefile improved, web pages regenerated

11 years agoChpater 4 and 5
Andrea Asperti [Mon, 11 Mar 2013 10:32:22 +0000 (10:32 +0000)]
Chpater 4 and 5

11 years ago- improved Makefile esp. with the "trim" function
Ferruccio Guidi [Sun, 10 Mar 2013 17:05:30 +0000 (17:05 +0000)]
- improved Makefile esp. with the "trim" function
- some files trimmed

11 years agochapters 2 e 3
Andrea Asperti [Sun, 10 Mar 2013 14:08:14 +0000 (14:08 +0000)]
chapters 2 e 3

11 years agowe removed a useless assertion that was forcing matita to edit just matita files
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!

11 years ago- update in basic_2
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

11 years agobasic_2_src.tbl was not updated :(
Ferruccio Guidi [Sat, 9 Mar 2013 22:26:54 +0000 (22:26 +0000)]
basic_2_src.tbl was not updated :(

11 years ago- lenv refinement for stratified native validity redefined
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

11 years agosecond recursive part of preservation finally proved!
Ferruccio Guidi [Fri, 8 Mar 2013 19:48:14 +0000 (19:48 +0000)]
second recursive part of preservation finally proved!

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 8 Mar 2013 13:47:28 +0000 (13:47 +0000)]
update in basic_2

11 years agoimproved "big treee" computation allows to close a case in the
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

11 years agoBug fixed: let-rec defined propositions are no longer extracted.
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.

11 years agoupdate in basic_2
Ferruccio Guidi [Sun, 3 Mar 2013 18:54:10 +0000 (18:54 +0000)]
update in basic_2

11 years ago- lambdadelta: we removed focalized reduction from snv preservation
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

11 years agoupdate in basic_2
Ferruccio Guidi [Thu, 28 Feb 2013 18:15:19 +0000 (18:15 +0000)]
update in basic_2

11 years ago- lambdadelta: first recursive part of preservation finally proved!
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)

11 years agochapter2 revisited
Andrea Asperti [Thu, 28 Feb 2013 16:22:28 +0000 (16:22 +0000)]
chapter2 revisited

11 years agoQuick patch: the maxmeta is now pushed/popped when compiling an external file.
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.

11 years agoQuick patch: the maxmeta is now pushed/popped when compiling an external file.
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.

11 years agoBug fixed: composite coercions were not extracted.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:18:18 +0000 (20:18 +0000)]
Bug fixed: composite coercions were not extracted.

11 years agoBug fixed that reveals a new one: in case of inductive types defined via
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.

11 years agoFerruccio's removal of objects commented out because it breaks compilation of
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!

11 years agoChapter 1 revisited
Andrea Asperti [Wed, 27 Feb 2013 16:48:15 +0000 (16:48 +0000)]
Chapter 1 revisited

11 years agowhen we serialize the contents of a .ma, we remove the old objects
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

11 years ago- xhtbl: now double quotes can appear in string literals
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

11 years ago- nUri : added Sets of uris for use in "probe"
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"

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 22 Feb 2013 21:54:29 +0000 (21:54 +0000)]
update in basic_2

11 years ago- "big tree" order implemented
Ferruccio Guidi [Fri, 22 Feb 2013 21:47:07 +0000 (21:47 +0000)]
- "big tree" order implemented
- some annotations

11 years agotrace added in a failing invocation of auto :-(
Ferruccio Guidi [Mon, 18 Feb 2013 21:50:27 +0000 (21:50 +0000)]
trace added in a failing invocation of auto :-(

11 years agoupdate in basic_2
Ferruccio Guidi [Mon, 18 Feb 2013 19:41:43 +0000 (19:41 +0000)]
update in basic_2

11 years agosubstitution lemma for stratified native validity!
Ferruccio Guidi [Mon, 18 Feb 2013 19:40:13 +0000 (19:40 +0000)]
substitution lemma for stratified native validity!

11 years agoupdate in basic_2 summary
Ferruccio Guidi [Fri, 15 Feb 2013 18:54:16 +0000 (18:54 +0000)]
update in basic_2 summary

11 years agowe rephrased sstas in terms of star
Ferruccio Guidi [Fri, 15 Feb 2013 18:52:30 +0000 (18:52 +0000)]
we rephrased sstas in terms of star

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 15 Feb 2013 14:21:51 +0000 (14:21 +0000)]
update in basic_2