2009-09-10 |
Enrico Tassi | nice hints |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | maledetto il \sub di CSC |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | it starts to work |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | nice notation for hints! |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | allow @{ ... } as the identifier of the letin |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | to me, the problem: |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Ferruccio Guidi | some interfaces improved |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | more stuff fixed |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | the refiner was not checking that the resulting type |
commit | commitdiff | tree | snapshot |
2009-09-09 |
Enrico Tassi | some fixes here and there |
commit | commitdiff | tree | snapshot |
2009-09-09 |
Enrico Tassi | depends |
commit | commitdiff | tree | snapshot |
2009-09-09 |
Enrico Tassi | some more work for ng-coercions |
commit | commitdiff | tree | snapshot |
2009-09-08 |
Ferruccio Guidi | some renaming and some interfaces improved |
commit | commitdiff | tree | snapshot |
2009-09-08 |
Enrico Tassi | snapshot for CSC |
commit | commitdiff | tree | snapshot |
2009-09-08 |
Enrico Tassi | snapshot for CSC |
commit | commitdiff | tree | snapshot |
2009-09-05 |
Ferruccio Guidi | basic_rg: more improvements to the error reporting... |
commit | commitdiff | tree | snapshot |
2009-09-05 |
Ferruccio Guidi | basic_rg: we improved the error reporting interface |
commit | commitdiff | tree | snapshot |
2009-09-04 |
Ferruccio Guidi | the TypeError exception is back in place inside the... |
commit | commitdiff | tree | snapshot |
2009-09-04 |
Enrico Tassi | Reduction speedup (a.k.a. better sharing): |
commit | commitdiff | tree | snapshot |
2009-09-04 |
Enrico Tassi | Reduction speedup (a.k.a. better sharing): |
commit | commitdiff | tree | snapshot |
2009-09-04 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-09-04 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-09-03 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-09-03 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-09-03 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-09-02 |
Enrico Tassi | fix to speedup reduction making intermediate conversion... |
commit | commitdiff | tree | snapshot |
2009-09-02 |
Enrico Tassi | fixed eliminator name |
commit | commitdiff | tree | snapshot |
2009-09-02 |
Enrico Tassi | some work |
commit | commitdiff | tree | snapshot |
2009-09-02 |
Enrico Tassi | CIC has no eta-reduction/expansion |
commit | commitdiff | tree | snapshot |
2009-09-02 |
Enrico Tassi | do not fail if the inductive type is mutual, just do... |
commit | commitdiff | tree | snapshot |
2009-09-02 |
Enrico Tassi | decent error on interpretation declaration |
commit | commitdiff | tree | snapshot |
2009-09-01 |
Enrico Tassi | fix double app in Ast |
commit | commitdiff | tree | snapshot |
2009-09-01 |
Enrico Tassi | better print of ILLEGAL applications |
commit | commitdiff | tree | snapshot |
2009-09-01 |
Ferruccio Guidi | lint target improved |
commit | commitdiff | tree | snapshot |
2009-09-01 |
Ferruccio Guidi | basic_rg: bugfix in AST to allow attributes in global... |
commit | commitdiff | tree | snapshot |
2009-09-01 |
Enrico Tassi | catch wrapped exception |
commit | commitdiff | tree | snapshot |
2009-08-28 |
Enrico Tassi | alias bug revealed |
commit | commitdiff | tree | snapshot |
2009-08-25 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-08-25 |
Enrico Tassi | initial and incomplete port of the old demo about induc... |
commit | commitdiff | tree | snapshot |
2009-08-25 |
Enrico Tassi | exponentiation should output with \sup not with ^,... |
commit | commitdiff | tree | snapshot |
2009-08-25 |
Enrico Tassi | added "already defined" |
commit | commitdiff | tree | snapshot |
2009-08-25 |
Enrico Tassi | ncoindutive now generates a co-inductive type, not... |
commit | commitdiff | tree | snapshot |
2009-08-25 |
Enrico Tassi | Meta case not handled, the iterator was complaining. |
commit | commitdiff | tree | snapshot |
2009-08-24 |
Claudio Sacerdoti... | Nicer proof "finished" (up to arithmetical facts). |
commit | commitdiff | tree | snapshot |
2009-08-23 |
Ferruccio Guidi | - alpha convertibility test disabled for now (it needs... |
commit | commitdiff | tree | snapshot |
2009-08-21 |
Claudio Sacerdoti... | Towards a simplified proof. |
commit | commitdiff | tree | snapshot |
2009-08-21 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-20 |
Claudio Sacerdoti... | Injectivity proved! What a mess... |
commit | commitdiff | tree | snapshot |
2009-08-20 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-20 |
Claudio Sacerdoti... | - Bug fixed in definition of big_op. |
commit | commitdiff | tree | snapshot |
2009-08-20 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-20 |
Ferruccio Guidi | - sort inclusion must be restricted to term backbone... |
commit | commitdiff | tree | snapshot |
2009-08-19 |
Claudio Sacerdoti... | One half done. |
commit | commitdiff | tree | snapshot |
2009-08-19 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-18 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-18 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-18 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-17 |
Ferruccio Guidi | - alpha conversion check added to the brg kernel (succe... |
commit | commitdiff | tree | snapshot |
2009-08-16 |
Ferruccio Guidi | - performance data added for reference |
commit | commitdiff | tree | snapshot |
2009-08-16 |
Ferruccio Guidi | - proper KAM with closures implemented for the brg... |
commit | commitdiff | tree | snapshot |
2009-08-15 |
Ferruccio Guidi | - kernel parameters indication added to exported object... |
commit | commitdiff | tree | snapshot |
2009-08-14 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-14 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-14 |
Claudio Sacerdoti... | Since the introduction of saturation, an assert false... |
commit | commitdiff | tree | snapshot |
2009-08-14 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Ferruccio Guidi | - xml exportation activated for the brg kernel |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Claudio Sacerdoti... | (nat,plus) is an abelian, unital magma |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Claudio Sacerdoti... | Some quick patch to fix elimination that used to look for |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Claudio Sacerdoti... | fix_sorts (cfr. previous commit) used to break too... |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Claudio Sacerdoti... | Assert false do not allow to debug... |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Claudio Sacerdoti... | Let's refresh the universe to avoid assert failure. |
commit | commitdiff | tree | snapshot |
2009-08-12 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-12 |
Claudio Sacerdoti... | A very little bit of arithmetic. |
commit | commitdiff | tree | snapshot |
2009-08-12 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-11 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-09 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-08 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-07 |
Ferruccio Guidi | basic_rg: improved interface, unwind removed from appli... |
commit | commitdiff | tree | snapshot |
2009-08-07 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-06 |
Claudio Sacerdoti... | The first omomorphism theorem for whole sets (i.e.... |
commit | commitdiff | tree | snapshot |
2009-08-06 |
Claudio Sacerdoti... | Hmmm: I don't see much gain here. |
commit | commitdiff | tree | snapshot |
2009-08-06 |
Claudio Sacerdoti... | Metas must be handled when using iterators. |
commit | commitdiff | tree | snapshot |
2009-08-06 |
Claudio Sacerdoti... | Setoid rewriting as unification hinting. Does not work... |
commit | commitdiff | tree | snapshot |
2009-08-06 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Claudio Sacerdoti... | More Gonthierism. Are they the right solution? |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Claudio Sacerdoti... | Hmmm, quite broken now. |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Cosimo Oliboni | freescle porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-03 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-01 |
Claudio Sacerdoti... | Smaller formulae. |
commit | commitdiff | tree | snapshot |
2009-08-01 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
next |