| 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 | new tactic constructor: @[n] |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | new syntax |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | let rec/corec and co/inductive are not printed! |
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 | allow @{ ... } as the identifier of the letin |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | to me, the problem: |
tree | commitdiff |
| 2009-09-10 |
Ferruccio Guidi | some interfaces improved |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | more stuff fixed |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | the refiner was not checking that the resulting type |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | some fixes here and there |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | depends |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | some more work for ng-coercions |
tree | commitdiff |
| 2009-09-08 |
Ferruccio Guidi | some renaming and some interfaces improved |
tree | commitdiff |
| 2009-09-08 |
Enrico Tassi | snapshot for CSC |
tree | commitdiff |
| 2009-09-08 |
Enrico Tassi | snapshot for CSC |
tree | commitdiff |
| 2009-09-05 |
Ferruccio Guidi | basic_rg: more improvements to the error reporting... |
tree | commitdiff |
| 2009-09-05 |
Ferruccio Guidi | basic_rg: we improved the error reporting interface |
tree | commitdiff |
| 2009-09-04 |
Ferruccio Guidi | the TypeError exception is back in place inside the... |
tree | commitdiff |
| 2009-09-04 |
Enrico Tassi | Reduction speedup (a.k.a. better sharing): |
tree | commitdiff |
| 2009-09-04 |
Enrico Tassi | Reduction speedup (a.k.a. better sharing): |
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-09-02 |
Enrico Tassi | do not fail if the inductive type is mutual, just do... |
tree | commitdiff |
| 2009-09-02 |
Enrico Tassi | decent error on interpretation declaration |
tree | commitdiff |
| 2009-09-01 |
Enrico Tassi | fix double app in Ast |
tree | commitdiff |
| 2009-09-01 |
Enrico Tassi | better print of ILLEGAL applications |
tree | commitdiff |
| 2009-09-01 |
Ferruccio Guidi | lint target improved |
tree | commitdiff |
| 2009-09-01 |
Ferruccio Guidi | basic_rg: bugfix in AST to allow attributes in global... |
tree | commitdiff |
| 2009-09-01 |
Enrico Tassi | catch wrapped exception |
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-25 |
Enrico Tassi | ncoindutive now generates a co-inductive type, not... |
tree | commitdiff |
| 2009-08-25 |
Enrico Tassi | Meta case not handled, the iterator was complaining. |
tree | commitdiff |
| 2009-08-24 |
Claudio Sacerdoti... | Nicer proof "finished" (up to arithmetical facts). |
tree | commitdiff |
| 2009-08-23 |
Ferruccio Guidi | - alpha convertibility test disabled for now (it needs... |
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-20 |
Ferruccio Guidi | - sort inclusion must be restricted to term backbone... |
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-17 |
Ferruccio Guidi | - alpha conversion check added to the brg kernel (succe... |
tree | commitdiff |
| 2009-08-16 |
Ferruccio Guidi | - performance data added for reference |
tree | commitdiff |
| 2009-08-16 |
Ferruccio Guidi | - proper KAM with closures implemented for the brg... |
tree | commitdiff |
| 2009-08-15 |
Ferruccio Guidi | - kernel parameters indication added to exported object... |
tree | commitdiff |
| 2009-08-14 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-14 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-08-14 |
Claudio Sacerdoti... | Since the introduction of saturation, an assert false... |
tree | commitdiff |
| 2009-08-14 |
Cosimo Oliboni | freescale porting, work in progress |
tree | commitdiff |
| 2009-08-13 |
Ferruccio Guidi | - xml exportation activated for the brg kernel |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | (nat,plus) is an abelian, unital magma |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | Some quick patch to fix elimination that used to look for |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | fix_sorts (cfr. previous commit) used to break too... |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | Assert false do not allow to debug... |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | Let's refresh the universe to avoid assert failure. |
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 |
Ferruccio Guidi | basic_rg: improved interface, unwind removed from appli... |
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... | Metas must be handled when using iterators. |
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 |
| next |
projects / helm.git / history