| 2009-09-14 |
Claudio Sacerdoti... | New tactics ncut and nlapply. |
tree | commitdiff |
| 2009-09-13 |
Enrico Tassi | a nice bug in meta handling is not visible... brr... |
tree | commitdiff |
| 2009-09-13 |
Enrico Tassi | some more letters |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | constructor accepts the arguments of the constructor... |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | new syntax |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | new macro ncheck. fixed term2pres for Inductive and... |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | ok, but slow on includes |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | nice hints |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | maledetto il \sub di CSC |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | it starts to work |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | nice notation for hints! |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | more stuff fixed |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | some more work for ng-coercions |
tree | commitdiff |
| 2009-09-08 |
Enrico Tassi | snapshot for CSC |
tree | commitdiff |
| 2009-09-04 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-09-04 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-09-03 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-09-03 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-09-03 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-09-02 |
Enrico Tassi | fix to speedup reduction making intermediate conversion... |
tree | commitdiff |
| 2009-09-02 |
Enrico Tassi | fixed eliminator name |
tree | commitdiff |
| 2009-09-02 |
Enrico Tassi | some work |
tree | commitdiff |
| 2009-09-02 |
Enrico Tassi | CIC has no eta-reduction/expansion |
tree | commitdiff |
| 2009-08-28 |
Enrico Tassi | alias bug revealed |
tree | commitdiff |
| 2009-08-25 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-08-25 |
Enrico Tassi | initial and incomplete port of the old demo about induc... |
tree | commitdiff |
| 2009-08-25 |
Enrico Tassi | exponentiation should output with \sup not with ^,... |
tree | commitdiff |
| 2009-08-25 |
Enrico Tassi | added "already defined" |
tree | commitdiff |
| 2009-08-24 |
Claudio Sacerdoti... | Nicer proof "finished" (up to arithmetical facts). |
tree | commitdiff |
| 2009-08-21 |
Claudio Sacerdoti... | Towards a simplified proof. |
tree | commitdiff |
| 2009-08-21 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-20 |
Claudio Sacerdoti... | Injectivity proved! What a mess... |
tree | commitdiff |
| 2009-08-20 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-20 |
Claudio Sacerdoti... | - Bug fixed in definition of big_op. |
tree | commitdiff |
| 2009-08-20 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-19 |
Claudio Sacerdoti... | One half done. |
tree | commitdiff |
| 2009-08-19 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-18 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-18 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-18 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-14 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-14 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-14 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | (nat,plus) is an abelian, unital magma |
tree | commitdiff |
| 2009-08-12 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-12 |
Claudio Sacerdoti... | A very little bit of arithmetic. |
tree | commitdiff |
| 2009-08-12 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-11 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-09 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-08 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-07 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-06 |
Claudio Sacerdoti... | The first omomorphism theorem for whole sets (i.e.... |
tree | commitdiff |
| 2009-08-06 |
Claudio Sacerdoti... | Hmmm: I don't see much gain here. |
tree | commitdiff |
| 2009-08-06 |
Claudio Sacerdoti... | Setoid rewriting as unification hinting. Does not work... |
tree | commitdiff |
| 2009-08-06 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-04 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-04 |
Claudio Sacerdoti... | More Gonthierism. Are they the right solution? |
tree | commitdiff |
| 2009-08-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-04 |
Claudio Sacerdoti... | Hmmm, quite broken now. |
tree | commitdiff |
| 2009-08-04 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-04 |
Cosimo Oliboni | freescle porting, work in progress |
tree | commitdiff |
| 2009-08-04 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-03 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-01 |
Claudio Sacerdoti... | Smaller formulae. |
tree | commitdiff |
| 2009-08-01 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-07-31 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-07-31 |
Claudio Sacerdoti... | Setoids, setoids1, sets, and the like. The mess begins. |
tree | commitdiff |
| 2009-07-31 |
Claudio Sacerdoti... | Record projections are now defined as fixpoints in... |
tree | commitdiff |
| 2009-07-30 |
Claudio Sacerdoti... | 1) \ldots here and there |
tree | commitdiff |
| 2009-07-30 |
Claudio Sacerdoti... | More napply \ldots => napply |
tree | commitdiff |
| 2009-07-30 |
Claudio Sacerdoti... | napply now automatically inserts \ldots at the end |
tree | commitdiff |
| 2009-07-30 |
Claudio Sacerdoti... | More \ldots. |
tree | commitdiff |
| 2009-07-30 |
Claudio Sacerdoti... | \ldots used here and there. Cool! |
tree | commitdiff |
| 2009-07-30 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-29 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-07-28 |
Claudio Sacerdoti... | Introduction of vectors of implicit (only for NG). |
tree | commitdiff |
| 2009-07-27 |
Claudio Sacerdoti... | Useless "let module" removed. |
tree | commitdiff |
| 2009-07-27 |
Claudio Sacerdoti... | Since I guess the divergence bug is fixed, I activate... |
tree | commitdiff |
| 2009-07-27 |
Claudio Sacerdoti... | setoids.ma split into setoids.ma + setoids1.ma |
tree | commitdiff |
| 2009-07-27 |
Claudio Sacerdoti... | topology/igt.ma (???) |-> sets/setoids.ma |
tree | commitdiff |
| 2009-07-27 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-24 |
Claudio Sacerdoti... | It works better now. |
tree | commitdiff |
| 2009-07-24 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-24 |
Claudio Sacerdoti... | No more hand-made coercions. |
tree | commitdiff |
| 2009-07-24 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-23 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-23 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-07-23 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-07-22 |
Claudio Sacerdoti... | Elimination principles are now processed in O(1) again |
tree | commitdiff |
| 2009-07-22 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-07-22 |
Claudio Sacerdoti... | 1) PTS simplified |
tree | commitdiff |
| 2009-07-22 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| next |
projects / helm.git / history