projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2011-05-20
Andrea Asperti
Simplified rendering.
commit
|
commitdiff
|
tree
|
snapshot
2011-05-20
Andrea Asperti
Simplified rendering
commit
|
commitdiff
|
tree
|
snapshot
2011-05-20
Andrea Asperti
Simplified rendering
commit
|
commitdiff
|
tree
|
snapshot
2011-05-20
Andrea Asperti
rm rendering attrs
commit
|
commitdiff
|
tree
|
snapshot
2011-05-20
Andrea Asperti
Removed mathml and proof rendering.
commit
|
commitdiff
|
tree
|
snapshot
2011-05-20
Andrea Asperti
Simplified rendering
commit
|
commitdiff
|
tree
|
snapshot
2011-05-20
Andrea Asperti
Porting to new reduction.
commit
|
commitdiff
|
tree
|
snapshot
2011-05-19
Wilmer Ricciotti
Added matitadaemon.
commit
|
commitdiff
|
tree
|
snapshot
2011-05-19
Ferruccio Guidi
cube.ma: some pts specifications of the lambda-cube
commit
|
commitdiff
|
tree
|
snapshot
2011-05-19
Andrea Asperti
Porting to the new pts.
commit
|
commitdiff
|
tree
|
snapshot
2011-05-19
Andrea Asperti
Porting to new parametric TJ.
commit
|
commitdiff
|
tree
|
snapshot
2011-05-19
Andrea Asperti
Dummies are blocked.
commit
|
commitdiff
|
tree
|
snapshot
2011-05-18
Andrea Asperti
New version of TJ parametric in the specification of...
commit
|
commitdiff
|
tree
|
snapshot
2011-05-14
Ferruccio Guidi
we added a property
commit
|
commitdiff
|
tree
|
snapshot
2011-05-13
Ferruccio Guidi
ground: some arithmetical properties added
commit
|
commitdiff
|
tree
|
snapshot
2011-05-13
Wilmer Ricciotti
interim version (added smallLexer)
commit
|
commitdiff
|
tree
|
snapshot
2011-05-12
Wilmer Ricciotti
Record projections:
commit
|
commitdiff
|
tree
|
snapshot
2011-05-12
Wilmer Ricciotti
Record projections:
commit
|
commitdiff
|
tree
|
snapshot
2011-05-11
Andrea Asperti
Partial modifications.
commit
|
commitdiff
|
tree
|
snapshot
2011-04-28
Ferruccio Guidi
we uncommented R3 and R4 tu be used in lambda-delta
commit
|
commitdiff
|
tree
|
snapshot
2011-04-28
Ferruccio Guidi
- weight: bugfix + weight-based eliminator axiomatized
commit
|
commitdiff
|
tree
|
snapshot
2011-04-21
Ferruccio Guidi
- we added notation for the zetable and thetable items
commit
|
commitdiff
|
tree
|
snapshot
2011-04-20
Andrea Asperti
convertibility.
commit
|
commitdiff
|
tree
|
snapshot
2011-04-20
Andrea Asperti
generatin lemmas and subject reduction (with a lot...
commit
|
commitdiff
|
tree
|
snapshot
2011-04-20
Andrea Asperti
progress
commit
|
commitdiff
|
tree
|
snapshot
2011-04-20
Andrea Asperti
error in the conversion rule
commit
|
commitdiff
|
tree
|
snapshot
2011-04-19
Ferruccio Guidi
notation bug fix
commit
|
commitdiff
|
tree
|
snapshot
2011-04-19
Ferruccio Guidi
- some bug fixes
commit
|
commitdiff
|
tree
|
snapshot
2011-04-19
Ferruccio Guidi
complete reformalization of lambda-delta in matita...
commit
|
commitdiff
|
tree
|
snapshot
2011-04-19
Ferruccio Guidi
disambiguation of explicit interprettions with argument...
commit
|
commitdiff
|
tree
|
snapshot
2011-04-13
Claudio Sacerdoti...
...
commit
|
commitdiff
|
tree
|
snapshot
2011-04-05
Ferruccio Guidi
we added an nmap from NCic.obj to NotationPt.obj (to...
commit
|
commitdiff
|
tree
|
snapshot
2011-04-05
Ferruccio Guidi
we removed an extra dot from the "include" syntax
commit
|
commitdiff
|
tree
|
snapshot
2011-04-04
Ferruccio Guidi
we introduced nterm for NotationPt.term
commit
|
commitdiff
|
tree
|
snapshot
2011-04-01
Claudio Sacerdoti...
Patch to avoid equations of the form ? -> T (oriented...
commit
|
commitdiff
|
tree
|
snapshot
2011-03-30
Ferruccio Guidi
we proved that the union of two saturated sets is saturated
commit
|
commitdiff
|
tree
|
snapshot
2011-03-30
Wilmer Ricciotti
Keeping track of locations of disambiguated ids and...
commit
|
commitdiff
|
tree
|
snapshot
2011-03-27
Claudio Sacerdoti...
Fixes previous wrong commit.
commit
|
commitdiff
|
tree
|
snapshot
2011-03-27
Claudio Sacerdoti...
1) Second half of the bug fixing for the "lexical keywo...
commit
|
commitdiff
|
tree
|
snapshot
2011-03-27
Claudio Sacerdoti...
Bug fixed: some Uri was not refreshed. The effect of...
commit
|
commitdiff
|
tree
|
snapshot
2011-03-27
Claudio Sacerdoti...
Debugging code commented out.
commit
|
commitdiff
|
tree
|
snapshot
2011-03-23
Ferruccio Guidi
- terms.ma: we included 'is_dummy" and "neutral" (maybe...
commit
|
commitdiff
|
tree
|
snapshot
2011-03-23
Claudio Sacerdoti...
More verbose in case of errors.
commit
|
commitdiff
|
tree
|
snapshot
2011-03-23
Andrea Asperti
red star
commit
|
commitdiff
|
tree
|
snapshot
2011-03-23
Claudio Sacerdoti...
Use jmeq from lib.
commit
|
commitdiff
|
tree
|
snapshot
2011-03-23
Claudio Sacerdoti...
Nested calls to matitac are now pretty-printed nicely.
commit
|
commitdiff
|
tree
|
snapshot
2011-03-22
Claudio Sacerdoti...
Reindentation.
commit
|
commitdiff
|
tree
|
snapshot
2011-03-22
Ferruccio Guidi
the weakening lemma is not needed since it is assumed...
commit
|
commitdiff
|
tree
|
snapshot
2011-03-22
Ferruccio Guidi
the thinning lemma follows immediately from the substit...
commit
|
commitdiff
|
tree
|
snapshot
2011-03-22
Ferruccio Guidi
- lambda_notation.ma: more notation and bug fixes
commit
|
commitdiff
|
tree
|
snapshot
2011-03-22
Claudio Sacerdoti...
Bug fixed and code refactoring: now both matitac and...
commit
|
commitdiff
|
tree
|
snapshot
2011-03-22
Claudio Sacerdoti...
Use matita/lib as the new standard library in place...
commit
|
commitdiff
|
tree
|
snapshot
2011-03-22
Claudio Sacerdoti...
Debugging code removed.
commit
|
commitdiff
|
tree
|
snapshot
2011-03-21
Andrea Asperti
sn_prod
commit
|
commitdiff
|
tree
|
snapshot
2011-03-21
Andrea Asperti
sn_lambda
commit
|
commitdiff
|
tree
|
snapshot
2011-03-21
Andrea Asperti
extensions
commit
|
commitdiff
|
tree
|
snapshot
2011-03-19
Claudio Sacerdoti...
Bug "fixed" (i.e avoided).
commit
|
commitdiff
|
tree
|
snapshot
2011-03-18
Claudio Sacerdoti...
Ported to
commit
|
commitdiff
|
tree
|
snapshot
2011-03-15
Ferruccio Guidi
- more notation and service lemmas
commit
|
commitdiff
|
tree
|
snapshot
2011-03-15
Ferruccio Guidi
- some ignores
commit
|
commitdiff
|
tree
|
snapshot
2011-03-14
Ferruccio Guidi
dependences fix
commit
|
commitdiff
|
tree
|
snapshot
2011-03-11
Andrea Asperti
added star.ma (star closure of a relation)
commit
|
commitdiff
|
tree
|
snapshot
2011-03-11
Andrea Asperti
Improvements.
commit
|
commitdiff
|
tree
|
snapshot
2011-03-10
Andrea Asperti
diamond property
commit
|
commitdiff
|
tree
|
snapshot
2011-03-09
Ferruccio Guidi
more notation and all-purpose lemmas
commit
|
commitdiff
|
tree
|
snapshot
2011-03-09
Ferruccio Guidi
the interpretation for Sigma was missing
commit
|
commitdiff
|
tree
|
snapshot
2011-03-08
Wilmer Ricciotti
First commit with new (incomplete) disambiguation engine.
commit
|
commitdiff
|
tree
|
snapshot
2011-03-07
Andrea Asperti
sottotermini e confluenza (manca pr_substs).
commit
|
commitdiff
|
tree
|
snapshot
2011-03-02
Ferruccio Guidi
we started the implementation of higher order saturated...
commit
|
commitdiff
|
tree
|
snapshot
2011-02-27
Ferruccio Guidi
- rc_sat.ma: we changed the notation for extensional...
commit
|
commitdiff
|
tree
|
snapshot
2011-02-27
Ferruccio Guidi
- notation is now in a separate file
commit
|
commitdiff
|
tree
|
snapshot
2011-02-26
Ferruccio Guidi
- new file ext.ma with the objects needed for the norma...
commit
|
commitdiff
|
tree
|
snapshot
2011-02-21
Ferruccio Guidi
we started to set up the strong normalization proof.
commit
|
commitdiff
|
tree
|
snapshot
2011-02-21
Wilmer Ricciotti
fork for Matita version B
commit
|
commitdiff
|
tree
|
snapshot
2011-02-10
Ferruccio Guidi
we added some comments
commit
|
commitdiff
|
tree
|
snapshot
2011-02-10
Andrea Asperti
Added typing rule for dummies
commit
|
commitdiff
|
tree
|
snapshot
2011-02-10
Andrea Asperti
Added lambda
commit
|
commitdiff
|
tree
|
snapshot
2011-02-09
Wilmer Ricciotti
enabling destruct defs
commit
|
commitdiff
|
tree
|
snapshot
2011-01-27
Claudio Sacerdoti...
Hyperlinks are back.
commit
|
commitdiff
|
tree
|
snapshot
2011-01-27
Claudio Sacerdoti...
Hyperlinks are now computed correctly. I least I hope...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-21
Wilmer Ricciotti
Removed inclusion of logic/equality.ma in datatypes...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-20
Wilmer Ricciotti
Bugfix for elimination principles.
commit
|
commitdiff
|
tree
|
snapshot
2011-01-20
Wilmer Ricciotti
Bug fix for generation of elimination principles.
commit
|
commitdiff
|
tree
|
snapshot
2011-01-19
Wilmer Ricciotti
Added some typing info to elimination principles, allow...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-19
Wilmer Ricciotti
Added some typing info to elimination principles, allow...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-14
Claudio Sacerdoti...
The sequent window now always scroll to the bottom...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-14
Claudio Sacerdoti...
Bug fixed: the script windows did not scroll correctly...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-11
Enrico Tassi
ctrl+pgUp/Down to navigate tabs
commit
|
commitdiff
|
tree
|
snapshot
2011-01-11
Enrico Tassi
ctrl+pgUp/Down to navigate tabs
commit
|
commitdiff
|
tree
|
snapshot
2011-01-11
Claudio Sacerdoti...
...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-11
Claudio Sacerdoti...
Bug fixed: the newScript method must be called only...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-11
Claudio Sacerdoti...
Bug fixed: the accelerators for Close and Quit were...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-11
Claudio Sacerdoti...
Last commit reverted (it was an error).
commit
|
commitdiff
|
tree
|
snapshot
2011-01-11
Claudio Sacerdoti...
Part of last HUGE COMMIT about NCic.status
commit
|
commitdiff
|
tree
|
snapshot
2011-01-11
Claudio Sacerdoti...
Stupid bug fixed (introduced a couple of commits ago...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-11
Claudio Sacerdoti...
HUGE COMMIT:
commit
|
commitdiff
|
tree
|
snapshot
2011-01-11
Enrico Tassi
coercion lookup now returns coercions ranked using...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-10
Claudio Sacerdoti...
code simplification
commit
|
commitdiff
|
tree
|
snapshot
2011-01-07
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2011-01-07
Enrico Tassi
added retrieval function with weight
commit
|
commitdiff
|
tree
|
snapshot
next