projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2013-04-08
Claudio Sacerdoti...
Patch by Paolo Tranquilli. It fixes the following probl...
commit
|
commitdiff
|
tree
|
snapshot
2013-04-08
matitaweb
commit by user andrea
commit
|
commitdiff
|
tree
|
snapshot
2013-04-07
Ferruccio Guidi
update in basic_2 and apps_2
commit
|
commitdiff
|
tree
|
snapshot
2013-04-07
Ferruccio Guidi
- new component for restricted computation (delta,...
commit
|
commitdiff
|
tree
|
snapshot
2013-04-05
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-04-05
Ferruccio Guidi
- parallel substitution reaxiomatized
commit
|
commitdiff
|
tree
|
snapshot
2013-03-20
Ferruccio Guidi
- probe: recursive removal of empty directories
commit
|
commitdiff
|
tree
|
snapshot
2013-03-18
Ferruccio Guidi
missing or rootless dependences now don't break the...
commit
|
commitdiff
|
tree
|
snapshot
2013-03-18
Ferruccio Guidi
some additions
commit
|
commitdiff
|
tree
|
snapshot
2013-03-18
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-03-18
Ferruccio Guidi
a file was added by mistake
commit
|
commitdiff
|
tree
|
snapshot
2013-03-18
Ferruccio Guidi
- more understanding of the "big tree" reduction step
commit
|
commitdiff
|
tree
|
snapshot
2013-03-17
Ferruccio Guidi
sfr renamed as lbotr and its symbol changed according...
commit
|
commitdiff
|
tree
|
snapshot
2013-03-17
Ferruccio Guidi
notational change for lsubr:
commit
|
commitdiff
|
tree
|
snapshot
2013-03-17
Ferruccio Guidi
lsubs renamed as lsubr
commit
|
commitdiff
|
tree
|
snapshot
2013-03-17
Ferruccio Guidi
notational change for snv and lsubsv: inverted "!"...
commit
|
commitdiff
|
tree
|
snapshot
2013-03-16
Ferruccio Guidi
milestone in basic_2!
commit
|
commitdiff
|
tree
|
snapshot
2013-03-16
Ferruccio Guidi
- lambdadelta: last recursive part of preservation...
commit
|
commitdiff
|
tree
|
snapshot
2013-03-14
Ferruccio Guidi
this is the real update :)
commit
|
commitdiff
|
tree
|
snapshot
2013-03-14
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-03-14
Ferruccio Guidi
- main proof case closed in the 4th component of preser...
commit
|
commitdiff
|
tree
|
snapshot
2013-03-13
Ferruccio Guidi
- lambdadelta: third recursive part of preservation...
commit
|
commitdiff
|
tree
|
snapshot
2013-03-11
Ferruccio Guidi
more results on lenv refinement for stratified native...
commit
|
commitdiff
|
tree
|
snapshot
2013-03-11
Ferruccio Guidi
bugfix in web tables
commit
|
commitdiff
|
tree
|
snapshot
2013-03-11
Ferruccio Guidi
some bugs fixed
commit
|
commitdiff
|
tree
|
snapshot
2013-03-11
Ferruccio Guidi
- xslt and Makefile improved, web pages regenerated
commit
|
commitdiff
|
tree
|
snapshot
2013-03-11
Andrea Asperti
Chpater 4 and 5
commit
|
commitdiff
|
tree
|
snapshot
2013-03-10
Ferruccio Guidi
- improved Makefile esp. with the "trim" function
commit
|
commitdiff
|
tree
|
snapshot
2013-03-10
Andrea Asperti
chapters 2 e 3
commit
|
commitdiff
|
tree
|
snapshot
2013-03-10
Ferruccio Guidi
we removed a useless assertion that was forcing matita...
commit
|
commitdiff
|
tree
|
snapshot
2013-03-09
Ferruccio Guidi
- update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-03-09
Ferruccio Guidi
basic_2_src.tbl was not updated :(
commit
|
commitdiff
|
tree
|
snapshot
2013-03-09
Ferruccio Guidi
- lenv refinement for stratified native validity redefined
commit
|
commitdiff
|
tree
|
snapshot
2013-03-08
Ferruccio Guidi
second recursive part of preservation finally proved!
commit
|
commitdiff
|
tree
|
snapshot
2013-03-08
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-03-08
Ferruccio Guidi
improved "big treee" computation allows to close a...
commit
|
commitdiff
|
tree
|
snapshot
2013-03-04
Claudio Sacerdoti...
Bug fixed: let-rec defined propositions are no longer...
commit
|
commitdiff
|
tree
|
snapshot
2013-03-03
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-03-03
Ferruccio Guidi
- lambdadelta: we removed focalized reduction from...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-28
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-02-28
Ferruccio Guidi
- lambdadelta: first recursive part of preservation...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-28
Andrea Asperti
chapter2 revisited
commit
|
commitdiff
|
tree
|
snapshot
2013-02-27
Claudio Sacerdoti...
Quick patch: the maxmeta is now pushed/popped when...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-27
Claudio Sacerdoti...
Quick patch: the maxmeta is now pushed/popped when...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-27
Claudio Sacerdoti...
Bug fixed: composite coercions were not extracted.
commit
|
commitdiff
|
tree
|
snapshot
2013-02-27
Claudio Sacerdoti...
Bug fixed that reveals a new one: in case of inductive...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-27
Claudio Sacerdoti...
Ferruccio's removal of objects commented out because...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-27
Andrea Asperti
Chapter 1 revisited
commit
|
commitdiff
|
tree
|
snapshot
2013-02-25
Ferruccio Guidi
when we serialize the contents of a .ma, we remove...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-24
Ferruccio Guidi
- xhtbl: now double quotes can appear in string literals
commit
|
commitdiff
|
tree
|
snapshot
2013-02-24
Ferruccio Guidi
- nUri : added Sets of uris for use in "probe"
commit
|
commitdiff
|
tree
|
snapshot
2013-02-22
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-02-22
Ferruccio Guidi
- "big tree" order implemented
commit
|
commitdiff
|
tree
|
snapshot
2013-02-18
Ferruccio Guidi
trace added in a failing invocation of auto :-(
commit
|
commitdiff
|
tree
|
snapshot
2013-02-18
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-02-18
Ferruccio Guidi
substitution lemma for stratified native validity!
commit
|
commitdiff
|
tree
|
snapshot
2013-02-15
Ferruccio Guidi
update in basic_2 summary
commit
|
commitdiff
|
tree
|
snapshot
2013-02-15
Ferruccio Guidi
we rephrased sstas in terms of star
commit
|
commitdiff
|
tree
|
snapshot
2013-02-15
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-02-15
Ferruccio Guidi
we reformulate the extended computation to simplify...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-13
Ferruccio Guidi
statistics update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-02-13
Ferruccio Guidi
- first piece of the mutual induction for preservation...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-11
Ferruccio Guidi
an update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-02-11
Ferruccio Guidi
more service lemmas in nat and lambdadelta
commit
|
commitdiff
|
tree
|
snapshot
2013-02-07
Ferruccio Guidi
one table was nissing ...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-07
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-02-07
Ferruccio Guidi
even more service lemmas ...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-07
Andrea Asperti
A few integrations
commit
|
commitdiff
|
tree
|
snapshot
2013-02-07
Andrea Asperti
restructuring
commit
|
commitdiff
|
tree
|
snapshot
2013-02-07
Andrea Asperti
(no commit message)
commit
|
commitdiff
|
tree
|
snapshot
2013-02-07
Andrea Asperti
restructuring
commit
|
commitdiff
|
tree
|
snapshot
2013-02-06
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-02-06
Ferruccio Guidi
- lambdadelta: more service lemmas ...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-05
Ferruccio Guidi
some missing files ...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-05
Claudio Sacerdoti...
Bug fixed: .ml/.mli files were opened/closed even when...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Claudio Sacerdoti...
Bug fixed: "open X" were not printed in .mli because...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Claudio Sacerdoti...
Flushing needed before closing the channel.
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Claudio Sacerdoti...
Improved exception handling.
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Claudio Sacerdoti...
Bug fixed in pretty printing of mutual inductive types.
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Claudio Sacerdoti...
Bug fixed: the indty can be typed with a Prod, not...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Claudio Sacerdoti...
New option -extract_ocaml to extract to ocaml files.
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Claudio Sacerdoti...
Pretty printing of ocaml files slightly improved.
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Claudio Sacerdoti...
Last known bug unrelated to names fixed: a fixpoint...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Wilmer Ricciotti
state mte2 renamed to mte_acc
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Claudio Sacerdoti...
...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Wilmer Ricciotti
converting certain basic machines to composed machines
commit
|
commitdiff
|
tree
|
snapshot
2013-02-04
Wilmer Ricciotti
defs.ma was never really used
commit
|
commitdiff
|
tree
|
snapshot
2013-02-02
Claudio Sacerdoti...
Makefile to extract to ocaml code.
commit
|
commitdiff
|
tree
|
snapshot
2013-02-02
Claudio Sacerdoti...
Oops, part of last commit (ocaml extraction implementation)
commit
|
commitdiff
|
tree
|
snapshot
2013-02-02
Claudio Sacerdoti...
Ooops, this completes the previous commit (ocaml extrac...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-02
Claudio Sacerdoti...
Implementation of Ocaml extraction (largely ported...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-02
Claudio Sacerdoti...
Identity change, improves readability.
commit
|
commitdiff
|
tree
|
snapshot
2013-02-01
Ferruccio Guidi
- Now the nodes count does not include the generated...
commit
|
commitdiff
|
tree
|
snapshot
2013-02-01
Ferruccio Guidi
lambda finaly moved in lib
commit
|
commitdiff
|
tree
|
snapshot
2013-02-01
Wilmer Ricciotti
match now only uses the new move operation
commit
|
commitdiff
|
tree
|
snapshot
2013-02-01
Ferruccio Guidi
- ng_refiner:
commit
|
commitdiff
|
tree
|
snapshot
2013-01-29
Wilmer Ricciotti
Speed-up in match.ma.
commit
|
commitdiff
|
tree
|
snapshot
2013-01-29
Wilmer Ricciotti
Proved old axiom.
commit
|
commitdiff
|
tree
|
snapshot
2013-01-29
Wilmer Ricciotti
Yippeee! Completes proof of soundness of the universal...
commit
|
commitdiff
|
tree
|
snapshot
2013-01-28
Andrea Asperti
unistep!!!
commit
|
commitdiff
|
tree
|
snapshot
next