2009-09-24 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-24 |
Enrico Tassi | multi screenshot |
commit | commitdiff | tree | snapshot |
2009-09-24 |
Enrico Tassi | ncheck works in the current ctx |
commit | commitdiff | tree | snapshot |
2009-09-24 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-24 |
Enrico Tassi | .... |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | more on screenshot |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | new macro screenshot |
commit | commitdiff | tree | snapshot |
2009-09-22 |
Ferruccio Guidi | we improved the stylesheets and we generated the static... |
commit | commitdiff | tree | snapshot |
2009-09-22 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Ferruccio Guidi | xml: bug fix |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Ferruccio Guidi | xml: first ld to xml stylesheets |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Enrico Tassi | new tactics by CSC |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Enrico Tassi | new implementation of delift_type_wrt_term, that call... |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Enrico Tassi | huge commit regarding universes: |
commit | commitdiff | tree | snapshot |
2009-09-18 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-09-17 |
Ferruccio Guidi | we start version 0.8.1 by replacing the abstract layer... |
commit | commitdiff | tree | snapshot |
2009-09-17 |
Enrico Tassi | one more exception printed |
commit | commitdiff | tree | snapshot |
2009-09-17 |
Enrico Tassi | more work for igft |
commit | commitdiff | tree | snapshot |
2009-09-16 |
Enrico Tassi | more notation for topologies, and some prentheses that... |
commit | commitdiff | tree | snapshot |
2009-09-16 |
Enrico Tassi | some more work... |
commit | commitdiff | tree | snapshot |
2009-09-16 |
Claudio Sacerdoti... | New interesting coercion. |
commit | commitdiff | tree | snapshot |
2009-09-16 |
Claudio Sacerdoti... | The left parameters coming from the constructor types... |
commit | commitdiff | tree | snapshot |
2009-09-15 |
Enrico Tassi | improved check in delift for flexible lc entries. |
commit | commitdiff | tree | snapshot |
2009-09-15 |
Ferruccio Guidi | some renaming. final commit for version 0.8.0 |
commit | commitdiff | tree | snapshot |
2009-09-14 |
Enrico Tassi | fixed coercion mechanism w.r.t. undo/require |
commit | commitdiff | tree | snapshot |
2009-09-14 |
Claudio Sacerdoti... | Slightly simplied status code. |
commit | commitdiff | tree | snapshot |
2009-09-14 |
Claudio Sacerdoti... | Simplest typing for status records. |
commit | commitdiff | tree | snapshot |
2009-09-14 |
Claudio Sacerdoti... | New tactics ncut and nlapply. |
commit | commitdiff | tree | snapshot |
2009-09-13 |
Enrico Tassi | a nice bug in meta handling is not visible... brr... |
commit | commitdiff | tree | snapshot |
2009-09-13 |
Enrico Tassi | some more letters |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | constructor accepts the arguments of the constructor... |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | new tactic constructor: @[n] |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | new syntax |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | let rec/corec and co/inductive are not printed! |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | new macro ncheck. fixed term2pres for Inductive and... |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | ok, but slow on includes |
commit | commitdiff | tree | snapshot |
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 |
next |