2009-10-06 |
Enrico Tassi | some fixes |
tree | commitdiff |
2009-10-06 |
Wilmer Ricciotti | Syntax highlighting for 'ninverter' keyword |
tree | commitdiff |
2009-10-06 |
Enrico Tassi | unification pps can be activated by the menu debug |
tree | commitdiff |
2009-10-05 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2009-10-05 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2009-10-05 |
Enrico Tassi | new ng_library module |
tree | commitdiff |
2009-10-05 |
Enrico Tassi | uffa |
tree | commitdiff |
2009-10-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2009-10-04 |
Claudio Sacerdoti... | Does not compile! Wrong unification hint? |
tree | commitdiff |
2009-10-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2009-10-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2009-10-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2009-10-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2009-10-02 |
Enrico Tassi | hints fixed |
tree | commitdiff |
2009-09-30 |
Claudio Sacerdoti... | With this hint, it diverges. |
tree | commitdiff |
2009-09-30 |
Claudio Sacerdoti... | New datatype for metasenv/subst: full fledged attribute... |
tree | commitdiff |
2009-09-29 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-29 |
Enrico Tassi | ugly coerc db print |
tree | commitdiff |
2009-09-29 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2009-09-29 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-29 |
Enrico Tassi | more virtuals |
tree | commitdiff |
2009-09-29 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-29 |
Claudio Sacerdoti... | It does not work recursively... |
tree | commitdiff |
2009-09-29 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2009-09-28 |
Enrico Tassi | non ho resistito! |
tree | commitdiff |
2009-09-28 |
Claudio Sacerdoti... | Experiment... |
tree | commitdiff |
2009-09-28 |
Claudio Sacerdoti... | Experiment... |
tree | commitdiff |
2009-09-25 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-25 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-25 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-24 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-24 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-24 |
Enrico Tassi | multi screenshot |
tree | commitdiff |
2009-09-24 |
Enrico Tassi | ncheck works in the current ctx |
tree | commitdiff |
2009-09-24 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-24 |
Enrico Tassi | .... |
tree | commitdiff |
2009-09-23 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-23 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-23 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-23 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-23 |
Enrico Tassi | more on screenshot |
tree | commitdiff |
2009-09-23 |
Enrico Tassi | new macro screenshot |
tree | commitdiff |
2009-09-22 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-21 |
Enrico Tassi | ... |
tree | commitdiff |
2009-09-21 |
Enrico Tassi | new tactics by CSC |
tree | commitdiff |
2009-09-21 |
Enrico Tassi | huge commit regarding universes: |
tree | commitdiff |
2009-09-18 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2009-09-17 |
Enrico Tassi | one more exception printed |
tree | commitdiff |
2009-09-17 |
Enrico Tassi | more work for igft |
tree | commitdiff |
2009-09-16 |
Enrico Tassi | more notation for topologies, and some prentheses that... |
tree | commitdiff |
2009-09-16 |
Enrico Tassi | some more work... |
tree | commitdiff |
2009-09-16 |
Claudio Sacerdoti... | New interesting coercion. |
tree | commitdiff |
2009-09-15 |
Enrico Tassi | improved check in delift for flexible lc entries. |
tree | commitdiff |
2009-09-14 |
Enrico Tassi | fixed coercion mechanism w.r.t. undo/require |
tree | commitdiff |
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 |
next |